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

Theorem 19.8a 1718
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 1716 . . 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  1727  19.23h  1728  19.2g  1780  19.9t  1782  excomim  1785  19.23t  1796  19.23bi  1802  19.38  1810  nexr  1820  qexmid  1827  sbequ1  1859  ax12olem5  1872  ax10lem2  1877  exdistrf  1911  ax11indn  2134  mo  2165  mo2  2172  euor2  2211  2moex  2214  2euex  2215  2moswap  2218  2mo  2221  rspe  2604  rsp2e  2606  ceqex  2898  mo2icl  2944  intab  3892  copsexg  4252  eusv2nf  4532  dmcosseq  4946  dminss  5095  imainss  5096  relssdmrn  5193  oprabid  5882  hta  7567  domtriomlem  8068  axextnd  8213  axrepnd  8216  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpownd  8223  axregndlem1  8224  axregnd  8226  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacndlem5  8233  axacnd  8234  fpwwe  8268  pwfseqlem4a  8283  pwfseqlem4  8284  reclem2pr  8672  amosym1  24865  copsexgb  24966  lppotos  26144  finminlem  26231  pm11.58  27589  ax10ext  27606  iotavalsb  27633  19.8ad  28187  vk15.4j  28291  onfrALTlem1  28313  onfrALTlem1VD  28666  vk15.4jVD  28690  bnj1121  29015  bnj1189  29039  ax12-2  29103  ax12OLD  29105  a12study5rev  29122  a12study11  29138  a12study11n  29139
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 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator