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

Theorem alnex 1533
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alnex  |-  ( A. x  -.  ph  <->  -.  E. x ph )

Proof of Theorem alnex
StepHypRef Expression
1 df-ex 1532 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
21con2bii 322 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wal 1530   E.wex 1531
This theorem is referenced by:  nex  1545  alex  1562  exim  1565  alinexa  1568  alexn  1569  nexdh  1579  19.35  1590  19.43  1595  19.43OLD  1596  19.33b  1598  nf4  1812  mo  2178  mo2  2185  2mo  2234  mo2icl  2957  disjsn  3706  dm0rn0  4911  reldm0  4912  iotanul  5250  imadif  5343  dffv2  5608  kmlem4  7795  axpowndlem3  8237  axpownd  8239  elfuns  24525  n0el  26828  pm10.251  27658  pm10.57  27669  2exnaln  27675  elnev  27741  nbusgra  28277  bnj1143  29138  a12lem2  29753  a12study10  29758  a12study10n  29759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator