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

Theorem alnex 1553
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 1552 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
21con2bii 324 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178   A.wal 1550   E.wex 1551
This theorem is referenced by:  nex  1565  alex  1582  exim  1585  alinexa  1589  alexn  1590  nexdh  1600  19.35  1611  19.43  1616  19.43OLD  1617  19.33b  1619  19.38  1813  nf4  1892  mo  2305  mo2  2312  2mo  2361  mo2icl  3115  disjsn  3870  dm0rn0  5088  reldm0  5089  iotanul  5435  imadif  5530  dffv2  5798  kmlem4  8035  axpowndlem3  8476  axpownd  8478  hashgt0elex  11672  nmo  23975  n0el  26710  pm10.251  27534  pm10.57  27545  2exnaln  27551  elnev  27617  bnj1143  29163
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 179  df-ex 1552
  Copyright terms: Public domain W3C validator