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

Theorem alnex 1532
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 1531 . 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 1529   E.wex 1530
This theorem is referenced by:  nex  1544  alex  1561  exim  1564  alinexa  1567  alexn  1568  nexdh  1578  19.35  1589  19.43  1594  19.43OLD  1595  19.33b  1597  nf4  1802  mo  2167  mo2  2174  2mo  2223  mo2icl  2946  disjsn  3695  dm0rn0  4897  reldm0  4898  iotanul  5236  imadif  5329  dffv2  5594  kmlem4  7781  axpowndlem3  8223  axpownd  8225  elfuns  24456  n0el  26736  pm10.251  27566  pm10.57  27577  2exnaln  27583  elnev  27649  nbusgra  28154  bnj1143  28895  a12lem2  29204  a12study10  29209  a12study10n  29210
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 1531
  Copyright terms: Public domain W3C validator