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

Theorem 19.8a 1912
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 1804 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1914. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
Assertion
Ref Expression
19.8a  |-  ( ph  ->  E. x ph )

Proof of Theorem 19.8a
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ax6ev 1800 . 2  |-  E. w  w  =  x
2 ax12v 1910 . . . . 5  |-  ( x  =  w  ->  ( ph  ->  A. x ( x  =  w  ->  ph )
) )
3 ax6ev 1800 . . . . 5  |-  E. x  x  =  w
4 exim 1700 . . . . 5  |-  ( A. x ( x  =  w  ->  ph )  -> 
( E. x  x  =  w  ->  E. x ph ) )
52, 3, 4syl6mpi 64 . . . 4  |-  ( x  =  w  ->  ( ph  ->  E. x ph )
)
65equcoms 1849 . . 3  |-  ( w  =  x  ->  ( ph  ->  E. x ph )
)
76exlimiv 1770 . 2  |-  ( E. w  w  =  x  ->  ( ph  ->  E. x ph ) )
81, 7ax-mp 5 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  sp  1914  19.2g  1923  19.23bi  1926  nexr  1927  19.9t  1946  19.9tOLD  1949  qexmid  2036  sbequ1  2050  ax6e  2060  exdistrf  2134  equvini  2146  2ax6e  2249  euor2  2313  2moex  2342  2euex  2343  2moswap  2346  2mo  2350  rspe  2880  rsp2eOLD  2882  ceqex  3201  mo2icl  3249  intab  4286  eusv2nf  4622  copsexg  4706  dmcosseq  5115  dminss  5269  imainss  5270  relssdmrn  5375  oprabid  6333  hta  8377  domtriomlem  8880  axextnd  9024  axrepnd  9027  axunndlem1  9028  axunnd  9029  axpowndlem2  9031  axpownd  9034  axregndlem1  9035  axregnd  9037  axacndlem1  9040  axacndlem2  9041  axacndlem3  9042  axacndlem4  9043  axacndlem5  9044  axacnd  9045  fpwwe  9079  pwfseqlem4a  9094  pwfseqlem4  9095  reclem2pr  9481  bnj1121  29803  bnj1189  29827  finminlem  30980  amosym1  31092  bj-19.23bit  31245  bj-nexrt  31246  bj-19.9htbi  31258  bj-nfdiOLD  31415  bj-finsumval0  31667  isbasisrelowllem1  31723  isbasisrelowllem2  31724  wl-exeq  31832  ax12indn  32484  pm11.58  36711  axc11next  36728  iotavalsb  36755  vk15.4j  36856  onfrALTlem1  36885  onfrALTlem1VD  37261  vk15.4jVD  37285  suprnmpt  37400  ssfiunibd  37482  ovncvrrp  38291  19.8ad  40088
  Copyright terms: Public domain W3C validator