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  2112  mo  2140  mo2  2147  euor2  2186  2moex  2189  2euex  2190  2moswap  2193  2mo  2196  ra4e  2579  ra42e  2581  ceqex  2873  mo2icl  2919  intab  3866  axnulALT  4121  copsexg  4224  eusv2nf  4504  dmcosseq  4934  dminss  5083  imainss  5084  relssdmrn  5180  tz6.12-1  5477  oprabid  5816  hta  7535  domtriomlem  8036  axextnd  8181  axrepnd  8184  axunndlem1  8185  axunnd  8186  axpowndlem2  8188  axpownd  8191  axregndlem1  8192  axregnd  8194  axacndlem1  8197  axacndlem2  8198  axacndlem3  8199  axacndlem4  8200  axacndlem5  8201  axacnd  8202  fpwwe  8236  pwfseqlem4a  8251  pwfseqlem4  8252  reclem2pr  8640  amosym1  24241  copsexgb  24333  lppotos  25512  finminlem  25599  pm11.58  26957  ax10ext  26974  iotavalsb  27002  19.8ad  27320  vk15.4j  27427  onfrALTlem1  27449  onfrALTlem1VD  27799  vk15.4jVD  27823  bnj1121  28147  bnj1189  28171  ax12-2  28353  ax12OLD  28355
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