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

Theorem 19.8a 1754
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 1663 . 2  |-  E. w  w  =  x
2 ax-17 1623 . . . . 5  |-  ( ph  ->  A. w ph )
3 ax-11 1753 . . . . 5  |-  ( x  =  w  ->  ( A. w ph  ->  A. x
( x  =  w  ->  ph ) ) )
4 a9ev 1663 . . . . . 6  |-  E. x  x  =  w
5 exim 1581 . . . . . 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 32 . . . 4  |-  ( x  =  w  ->  ( ph  ->  E. x ph )
)
87equcoms 1688 . . 3  |-  ( w  =  x  ->  ( ph  ->  E. x ph )
)
98exlimiv 1641 . 2  |-  ( E. w  w  =  x  ->  ( ph  ->  E. x ph ) )
101, 9ax-mp 8 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546   E.wex 1547
This theorem is referenced by:  sp  1755  19.2g  1765  19.23bi  1767  nexr  1768  19.9t  1787  19.9hOLD  1789  19.23tOLD  1828  19.23hOLD  1829  19.9tOLD  1869  excomimOLD  1870  19.38OLD  1884  qexmid  1897  sbequ1  1932  a9e  1941  ax12olem5OLD  1969  ax10lem2OLD  1983  exdistrf  2010  ax11indn  2229  mo  2260  mo2  2267  euor2  2306  2moex  2309  2euex  2310  2moswap  2313  2mo  2316  rspe  2710  rsp2e  2712  ceqex  3009  mo2icl  3056  intab  4022  copsexg  4383  eusv2nf  4661  dmcosseq  5077  dminss  5226  imainss  5227  relssdmrn  5330  oprabid  6044  hta  7754  domtriomlem  8255  axextnd  8399  axrepnd  8402  axunndlem1  8403  axunnd  8404  axpowndlem2  8406  axpownd  8409  axregndlem1  8410  axregnd  8412  axacndlem1  8415  axacndlem2  8416  axacndlem3  8417  axacndlem4  8418  axacndlem5  8419  axacnd  8420  fpwwe  8454  pwfseqlem4a  8469  pwfseqlem4  8470  reclem2pr  8858  amosym1  25890  finminlem  26012  pm11.58  27258  ax10ext  27275  iotavalsb  27302  19.8ad  27806  vk15.4j  27955  onfrALTlem1  27977  onfrALTlem1VD  28343  vk15.4jVD  28367  bnj1121  28692  bnj1189  28716  exdistrfNEW7  28843  excomimOLD7  29009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator