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  2135  mo2  2142  2mo  2191  mo2icl  2881  disjsn  3597  dm0rn0  4802  reldm0  4803  imadif  5184  dffv2  5444  iotanul  6158  kmlem4  7663  axpowndlem3  8101  axpownd  8103  n0el  25891  pm10.251  26721  pm10.57  26732  2exnaln  26738  elnev  26805  bnj1143  27511  a12lem2  27820  a12study10  27825  a12study10n  27826
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