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  1971  ax10lem2OLD  1985  exdistrf  2012  ax11indn  2230  mo  2261  mo2  2268  euor2  2307  2moex  2310  2euex  2311  2moswap  2314  2mo  2317  rspe  2711  rsp2e  2713  ceqex  3010  mo2icl  3057  intab  4023  copsexg  4384  eusv2nf  4662  dmcosseq  5078  dminss  5227  imainss  5228  relssdmrn  5331  oprabid  6045  hta  7755  domtriomlem  8256  axextnd  8400  axrepnd  8403  axunndlem1  8404  axunnd  8405  axpowndlem2  8407  axpownd  8410  axregndlem1  8411  axregnd  8413  axacndlem1  8416  axacndlem2  8417  axacndlem3  8418  axacndlem4  8419  axacndlem5  8420  axacnd  8421  fpwwe  8455  pwfseqlem4a  8470  pwfseqlem4  8471  reclem2pr  8859  amosym1  25891  finminlem  26013  pm11.58  27259  ax10ext  27276  iotavalsb  27303  19.8ad  27807  vk15.4j  27956  onfrALTlem1  27978  onfrALTlem1VD  28344  vk15.4jVD  28368  bnj1121  28693  bnj1189  28717  exdistrfNEW7  28844  excomimOLD7  29010
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