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

Theorem alnex 1530
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 1529 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
21con2bii 322 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wal 1527   E.wex 1528
This theorem is referenced by:  nex  1542  alex  1559  exim  1562  alinexa  1565  alexn  1566  nexdh  1576  19.35  1587  19.43  1592  19.43OLD  1593  19.33b  1595  nf4  1802  mo  2166  mo2  2173  2mo  2222  mo2icl  2945  disjsn  3694  dm0rn0  4894  reldm0  4895  imadif  5293  dffv2  5554  iotanul  6268  kmlem4  7775  axpowndlem3  8217  axpownd  8219  n0el  26136  pm10.251  26966  pm10.57  26977  2exnaln  26983  elnev  27049  bnj1143  28101  a12lem2  28410  a12study10  28415  a12study10n  28416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator