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

Theorem 19.8a 1762
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 1668 . 2  |-  E. w  w  =  x
2 ax-17 1626 . . . . 5  |-  ( ph  ->  A. w ph )
3 ax-11 1761 . . . . 5  |-  ( x  =  w  ->  ( A. w ph  ->  A. x
( x  =  w  ->  ph ) ) )
4 a9ev 1668 . . . . . 6  |-  E. x  x  =  w
5 exim 1584 . . . . . 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 1693 . . 3  |-  ( w  =  x  ->  ( ph  ->  E. x ph )
)
98exlimiv 1644 . 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 1549   E.wex 1550
This theorem is referenced by:  sp  1763  19.2g  1773  19.23bi  1775  nexr  1776  19.9t  1793  19.9hOLD  1795  19.23tOLD  1838  19.23hOLD  1839  19.9tOLD  1880  excomimOLD  1881  19.38OLD  1895  qexmid  1908  sbequ1  1943  a9e  1952  ax12olem5OLD  2015  ax10lem2OLD  2026  exdistrf  2062  exdistrfOLD  2063  ax11indn  2271  mo  2302  mo2  2309  euor2  2348  2moex  2351  2euex  2352  2moswap  2355  2mo  2358  rspe  2754  rsp2e  2756  ceqex  3053  mo2icl  3100  intab  4067  copsexg  4429  eusv2nf  4707  dmcosseq  5123  dminss  5272  imainss  5273  relssdmrn  5376  oprabid  6091  hta  7805  domtriomlem  8306  axextnd  8450  axrepnd  8453  axunndlem1  8454  axunnd  8455  axpowndlem2  8457  axpownd  8460  axregndlem1  8461  axregnd  8463  axacndlem1  8466  axacndlem2  8467  axacndlem3  8468  axacndlem4  8469  axacndlem5  8470  axacnd  8471  fpwwe  8505  pwfseqlem4a  8520  pwfseqlem4  8521  reclem2pr  8909  amosym1  26119  wl-exeq  26177  finminlem  26253  pm11.58  27499  ax10ext  27516  iotavalsb  27543  19.8ad  28216  vk15.4j  28365  onfrALTlem1  28387  onfrALTlem1VD  28754  vk15.4jVD  28778  bnj1121  29106  bnj1189  29130  exdistrfNEW7  29257  excomimOLD7  29423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator