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

Theorem 19.8a 1764
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 13-Jan-2018.)
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 a9ev 1670 . 2  |-  E. w  w  =  x
2 ax-17 1627 . . . . 5  |-  ( ph  ->  A. w ph )
3 ax-11 1763 . . . . 5  |-  ( x  =  w  ->  ( A. w ph  ->  A. x
( x  =  w  ->  ph ) ) )
4 a9ev 1670 . . . . . 6  |-  E. x  x  =  w
5 exim 1585 . . . . . 6  |-  ( A. x ( x  =  w  ->  ph )  -> 
( E. x  x  =  w  ->  E. x ph ) )
64, 5mpi 17 . . . . 5  |-  ( A. x ( x  =  w  ->  ph )  ->  E. x ph )
72, 3, 6syl56 33 . . . 4  |-  ( x  =  w  ->  ( ph  ->  E. x ph )
)
87equcoms 1695 . . 3  |-  ( w  =  x  ->  ( ph  ->  E. x ph )
)
98exlimiv 1645 . 2  |-  ( E. w  w  =  x  ->  ( ph  ->  E. x ph ) )
101, 9ax-mp 5 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   E.wex 1551
This theorem is referenced by:  sp  1765  19.2g  1775  19.23bi  1777  nexr  1778  19.9t  1795  19.9hOLD  1797  19.23tOLD  1840  19.23hOLD  1841  19.9tOLD  1882  excomimOLD  1883  nfdi  1894  19.38OLD  1898  qexmid  1911  sbequ1  1946  a9e  1955  ax12olem5OLD  2018  ax10lem2OLD  2029  exdistrf  2069  exdistrfOLD  2070  ax11indn  2278  mo  2309  mo2  2316  euor2  2355  2moex  2358  2euex  2359  2moswap  2362  2mo  2365  rspe  2773  rsp2e  2775  ceqex  3072  mo2icl  3119  intab  4104  copsexg  4471  eusv2nf  4750  dmcosseq  5166  dminss  5315  imainss  5316  relssdmrn  5419  oprabid  6134  hta  7852  domtriomlem  8353  axextnd  8497  axrepnd  8500  axunndlem1  8501  axunnd  8502  axpowndlem2  8504  axpownd  8507  axregndlem1  8508  axregnd  8510  axacndlem1  8513  axacndlem2  8514  axacndlem3  8515  axacndlem4  8516  axacndlem5  8517  axacnd  8518  fpwwe  8552  pwfseqlem4a  8567  pwfseqlem4  8568  reclem2pr  8956  amosym1  26207  wl-exeq  26265  finminlem  26359  pm11.58  27604  ax10ext  27621  iotavalsb  27648  19.8ad  28558  vk15.4j  28710  onfrALTlem1  28732  onfrALTlem1VD  29100  vk15.4jVD  29124  bnj1121  29452  bnj1189  29476  exdistrfNEW7  29603  excomimOLD7  29791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator