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  1800  mo  2165  mo2  2172  2mo  2221  mo2icl  2944  disjsn  3693  dm0rn0  4895  reldm0  4896  iotanul  5234  imadif  5327  dffv2  5592  kmlem4  7779  axpowndlem3  8221  axpownd  8223  elfuns  24454  n0el  26725  pm10.251  27555  pm10.57  27566  2exnaln  27572  elnev  27638  nbusgra  28143  bnj1143  28822  a12lem2  29131  a12study10  29136  a12study10n  29137
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