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  1863  sbequ1  1889  ax11indn  2108  mo  2135  mo2  2142  euor2  2181  2moex  2184  2euex  2185  2moswap  2188  2mo  2191  ra4e  2566  ra42e  2568  ceqex  2835  mo2icl  2881  intab  3790  axnulALT  4044  copsexg  4145  eusv2nf  4423  dmcosseq  4853  dminss  5002  imainss  5003  relssdmrn  5099  tz6.12-1  5396  oprabid  5734  hta  7451  domtriomlem  7952  axextnd  8093  axrepnd  8096  axunndlem1  8097  axunnd  8098  axpowndlem2  8100  axpownd  8103  axregndlem1  8104  axregnd  8106  axacndlem1  8109  axacndlem2  8110  axacndlem3  8111  axacndlem4  8112  axacndlem5  8113  axacnd  8114  fpwwe  8148  pwfseqlem4a  8163  pwfseqlem4  8164  reclem2pr  8552  amosym1  24039  copsexgb  24131  lppotos  25310  finminlem  25397  pm11.58  26755  ax10ext  26772  iotavalsb  26800  19.8ad  26876  vk15.4j  26984  onfrALTlem1  27006  onfrALTlem1VD  27356  vk15.4jVD  27380  bnj1121  27704  bnj1189  27728  ax12-2  27792  ax12OLD  27794
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