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

Theorem alnex 1549
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 1548 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
21con2bii 323 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wal 1546   E.wex 1547
This theorem is referenced by:  nex  1561  alex  1578  exim  1581  alinexa  1585  alexn  1586  nexdh  1596  19.35  1607  19.43  1612  19.43OLD  1613  19.33b  1615  19.38  1802  nf4  1880  mo  2260  mo2  2267  2mo  2316  axi11e  2366  mo2icl  3056  disjsn  3811  dm0rn0  5026  reldm0  5027  iotanul  5373  imadif  5468  dffv2  5735  kmlem4  7966  axpowndlem3  8407  axpownd  8409  hashgt0elex  11597  nbusgra  21306  nmo  23817  elfuns  25478  n0el  26399  pm10.251  27224  pm10.57  27235  2exnaln  27241  elnev  27307  bnj1143  28499
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 178  df-ex 1548
  Copyright terms: Public domain W3C validator