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  5089  reldm0  5090  iotanul  5436  imadif  5531  dffv2  5799  kmlem4  8038  axpowndlem3  8479  axpownd  8481  hashgt0elex  11675  nmo  23978  n0el  26722  pm10.251  27546  pm10.57  27557  2exnaln  27563  elnev  27629  bnj1143  29235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator