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 1718 . . 3  |-  ( A. x  -.  ph  ->  -.  ph )
21con2i 112 . 2  |-  ( ph  ->  -.  A. x  -.  ph )
3 df-ex 1531 . 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 1529   E.wex 1530
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  1913  ax11indn  2136  mo  2167  mo2  2174  euor2  2213  2moex  2216  2euex  2217  2moswap  2220  2mo  2223  rspe  2606  rsp2e  2608  ceqex  2900  mo2icl  2946  intab  3894  copsexg  4254  eusv2nf  4534  dmcosseq  4948  dminss  5097  imainss  5098  relssdmrn  5195  oprabid  5884  hta  7569  domtriomlem  8070  axextnd  8215  axrepnd  8218  axunndlem1  8219  axunnd  8220  axpowndlem2  8222  axpownd  8225  axregndlem1  8226  axregnd  8228  axacndlem1  8231  axacndlem2  8232  axacndlem3  8233  axacndlem4  8234  axacndlem5  8235  axacnd  8236  fpwwe  8270  pwfseqlem4a  8285  pwfseqlem4  8286  reclem2pr  8674  amosym1  24867  copsexgb  24977  lppotos  26155  finminlem  26242  pm11.58  27600  ax10ext  27617  iotavalsb  27644  19.8ad  28198  vk15.4j  28347  onfrALTlem1  28369  onfrALTlem1VD  28739  vk15.4jVD  28763  bnj1121  29088  bnj1189  29112  ax12-2  29176  ax12OLD  29178  a12study5rev  29195  a12study11  29211  a12study11n  29212
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-ex 1531
  Copyright terms: Public domain W3C validator