MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8a Structured version   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  2759  rsp2e  2761  ceqex  3058  mo2icl  3105  intab  4072  copsexg  4434  eusv2nf  4713  dmcosseq  5129  dminss  5278  imainss  5279  relssdmrn  5382  oprabid  6097  hta  7813  domtriomlem  8314  axextnd  8458  axrepnd  8461  axunndlem1  8462  axunnd  8463  axpowndlem2  8465  axpownd  8468  axregndlem1  8469  axregnd  8471  axacndlem1  8474  axacndlem2  8475  axacndlem3  8476  axacndlem4  8477  axacndlem5  8478  axacnd  8479  fpwwe  8513  pwfseqlem4a  8528  pwfseqlem4  8529  reclem2pr  8917  amosym1  26168  wl-exeq  26226  finminlem  26312  pm11.58  27557  ax10ext  27574  iotavalsb  27601  19.8ad  28397  vk15.4j  28549  onfrALTlem1  28571  onfrALTlem1VD  28939  vk15.4jVD  28963  bnj1121  29291  bnj1189  29315  exdistrfNEW7  29442  excomimOLD7  29630
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