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

Theorem 19.8a 1758
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 ax-4 1692 . . 3  |-  ( A. x  -.  ph  ->  -.  ph )
21con2i 114 . 2  |-  ( ph  ->  -.  A. x  -.  ph )
3 df-ex 1538 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
42, 3sylibr 205 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532   E.wex 1537
This theorem is referenced by:  19.2  1759  19.9t  1761  excomim  1764  19.23t  1776  19.23bi  1783  19.38  1791  nexr  1804  qexmid  1813  exdistrf  1864  sbequ1  1890  ax11indn  2111  mo  2138  mo2  2145  euor2  2184  2moex  2187  2euex  2188  2moswap  2191  2mo  2194  ra4e  2575  ra42e  2577  ceqex  2849  mo2icl  2895  intab  3833  axnulALT  4087  copsexg  4189  eusv2nf  4469  dmcosseq  4899  dminss  5048  imainss  5049  relssdmrn  5145  tz6.12-1  5442  oprabid  5781  hta  7500  domtriomlem  8001  axextnd  8146  axrepnd  8149  axunndlem1  8150  axunnd  8151  axpowndlem2  8153  axpownd  8156  axregndlem1  8157  axregnd  8159  axacndlem1  8162  axacndlem2  8163  axacndlem3  8164  axacndlem4  8165  axacndlem5  8166  axacnd  8167  fpwwe  8201  pwfseqlem4a  8216  pwfseqlem4  8217  reclem2pr  8605  amosym1  24205  copsexgb  24297  lppotos  25476  finminlem  25563  pm11.58  26921  ax10ext  26938  iotavalsb  26966  19.8ad  27199  vk15.4j  27307  onfrALTlem1  27329  onfrALTlem1VD  27679  vk15.4jVD  27703  bnj1121  28027  bnj1189  28051  ax12-2  28233  ax12OLD  28235
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-ex 1538
  Copyright terms: Public domain W3C validator