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

Theorem alnex 1569
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 1538 . 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 5    <-> wb 178   A.wal 1532   E.wex 1537
This theorem is referenced by:  alex  1570  exim  1573  alinexa  1576  alexn  1577  nex  1587  nexdh  1588  19.35  1599  19.43  1604  19.43OLD  1605  19.33b  1607  nf4  1780  mo  2138  mo2  2145  2mo  2194  mo2icl  2912  disjsn  3653  dm0rn0  4869  reldm0  4870  imadif  5251  dffv2  5512  iotanul  6226  kmlem4  7733  axpowndlem3  8175  axpownd  8177  n0el  26078  pm10.251  26908  pm10.57  26919  2exnaln  26925  elnev  26992  bnj1143  27855  a12lem2  28282  a12study10  28287  a12study10n  28288
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-ex 1538
  Copyright terms: Public domain W3C validator