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

Theorem 19.8a 1730
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 1728 . . 3  |-  ( A. x  -.  ph  ->  -.  ph )
21con2i 112 . 2  |-  ( ph  ->  -.  A. x  -.  ph )
3 df-ex 1532 . 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 1530   E.wex 1531
This theorem is referenced by:  19.9h  1739  19.23h  1740  19.2g  1792  19.9t  1794  excomim  1797  19.23t  1808  19.23bi  1814  19.38  1822  nexr  1832  qexmid  1839  sbequ1  1871  ax12olem5  1884  ax10lem2  1890  exdistrf  1924  ax11indn  2147  mo  2178  mo2  2185  euor2  2224  2moex  2227  2euex  2228  2moswap  2231  2mo  2234  rspe  2617  rsp2e  2619  ceqex  2911  mo2icl  2957  intab  3908  copsexg  4268  eusv2nf  4548  dmcosseq  4962  dminss  5111  imainss  5112  relssdmrn  5209  oprabid  5898  hta  7583  domtriomlem  8084  axextnd  8229  axrepnd  8232  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpownd  8239  axregndlem1  8240  axregnd  8242  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacndlem5  8249  axacnd  8250  fpwwe  8284  pwfseqlem4a  8299  pwfseqlem4  8300  reclem2pr  8688  amosym1  24937  copsexgb  25069  lppotos  26247  finminlem  26334  pm11.58  27692  ax10ext  27709  iotavalsb  27736  19.8ad  28441  vk15.4j  28590  onfrALTlem1  28612  onfrALTlem1VD  28982  vk15.4jVD  29006  bnj1121  29331  bnj1189  29355  exdistrfNEW7  29482  excomimOLD7  29647  ax12-2  29725  ax12OLD  29727  a12study5rev  29744  a12study11  29760  a12study11n  29761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator