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

Theorem 19.8a 1720
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.)
Assertion
Ref Expression
19.8a  |-  ( ph  ->  E. x ph )

Proof of Theorem 19.8a
StepHypRef Expression
1 sp 1717 . . 3  |-  ( A. x  -.  ph  ->  -.  ph )
21con2i 112 . 2  |-  ( ph  ->  -.  A. x  -.  ph )
3 df-ex 1529 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
42, 3sylibr 203 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527   E.wex 1528
This theorem is referenced by:  19.9h  1729  19.23h  1730  19.2g  1782  19.9t  1784  excomim  1787  19.23t  1798  19.23bi  1804  19.38  1812  nexr  1822  qexmid  1829  sbequ1  1861  ax12olem5  1874  ax10lem2  1879  exdistrf  1914  ax11indn  2135  mo  2166  mo2  2173  euor2  2212  2moex  2215  2euex  2216  2moswap  2219  2mo  2222  rspe  2605  rsp2e  2607  ceqex  2899  mo2icl  2945  intab  3893  axnulALT  4148  copsexg  4251  eusv2nf  4531  dmcosseq  4945  dminss  5094  imainss  5095  relssdmrn  5191  tz6.12-1  5505  oprabid  5844  hta  7563  domtriomlem  8064  axextnd  8209  axrepnd  8212  axunndlem1  8213  axunnd  8214  axpowndlem2  8216  axpownd  8219  axregndlem1  8220  axregnd  8222  axacndlem1  8225  axacndlem2  8226  axacndlem3  8227  axacndlem4  8228  axacndlem5  8229  axacnd  8230  fpwwe  8264  pwfseqlem4a  8279  pwfseqlem4  8280  reclem2pr  8668  amosym1  24275  copsexgb  24376  lppotos  25555  finminlem  25642  pm11.58  27000  ax10ext  27017  iotavalsb  27044  19.8ad  27459  vk15.4j  27574  onfrALTlem1  27596  onfrALTlem1VD  27946  vk15.4jVD  27970  bnj1121  28294  bnj1189  28318  ax12-2  28382  ax12OLD  28384  a12study5rev  28401  a12study11  28417  a12study11n  28418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator