MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8a Structured version   Visualization version   GIF version

Theorem 19.8a 1988
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 1843 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1990. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
Assertion
Ref Expression
19.8a (𝜑 → ∃𝑥𝜑)

Proof of Theorem 19.8a
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ax12v 1984 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1838 . . 3 𝑥 𝑥 = 𝑦
3 exim 1737 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 64 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1891 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1808 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1466  wex 1692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-12 1983
This theorem depends on definitions:  df-bi 192  df-ex 1693
This theorem is referenced by:  sp  1990  19.2g  1999  19.23bi  2002  nexr  2003  19.9t  2022  19.9tOLD  2025  qexmid  2109  sbequ1  2130  ax6e  2141  exdistrf  2216  equvini  2229  2ax6e  2333  euor2  2397  2moex  2426  2euex  2427  2moswap  2430  2mo  2434  rspe  2879  ceqex  3192  mo2icl  3241  intab  4294  eusv2nf  4640  copsexg  4728  dmcosseq  5145  dminss  5300  imainss  5301  relssdmrn  5407  oprabid  6390  hta  8453  domtriomlem  8957  axextnd  9101  axrepnd  9104  axunndlem1  9105  axunnd  9106  axpowndlem2  9108  axpownd  9111  axregndlem1  9112  axregnd  9114  axacndlem1  9117  axacndlem2  9118  axacndlem3  9119  axacndlem4  9120  axacndlem5  9121  axacnd  9122  fpwwe  9156  pwfseqlem4a  9171  pwfseqlem4  9172  reclem2pr  9558  bnj1121  29946  bnj1189  29970  finminlem  31123  amosym1  31235  bj-ssbft  31437  bj-19.23bit  31469  bj-nexrt  31470  bj-19.9htbi  31482  bj-sbsb  31621  bj-nfdiOLD  31628  bj-xnex  31844  bj-finsumval0  31923  isbasisrelowllem1  31979  isbasisrelowllem2  31980  wl-exeq  32098  ax12indn  32747  gneispace  36930  pm11.58  37097  axc11next  37114  iotavalsb  37141  vk15.4j  37241  onfrALTlem1  37270  onfrALTlem1VD  37635  vk15.4jVD  37659  suprnmpt  37802  ssfiunibd  37904  ovncvrrp  38849  19.8ad  41626
  Copyright terms: Public domain W3C validator