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  2140  mo2  2147  2mo  2196  mo2icl  2919  disjsn  3667  dm0rn0  4883  reldm0  4884  imadif  5265  dffv2  5526  iotanul  6240  kmlem4  7747  axpowndlem3  8189  axpownd  8191  n0el  26093  pm10.251  26923  pm10.57  26934  2exnaln  26940  elnev  27007  bnj1143  27954  a12lem2  28381  a12study10  28386  a12study10n  28387
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