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  2895  disjsn  3634  dm0rn0  4848  reldm0  4849  imadif  5230  dffv2  5491  iotanul  6205  kmlem4  7712  axpowndlem3  8154  axpownd  8156  n0el  26057  pm10.251  26887  pm10.57  26898  2exnaln  26904  elnev  26971  bnj1143  27834  a12lem2  28261  a12study10  28266  a12study10n  28267
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