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  1808  nf4  1887  mo  2280  mo2  2287  2mo  2336  axi11e  2386  mo2icl  3077  disjsn  3832  dm0rn0  5049  reldm0  5050  iotanul  5396  imadif  5491  dffv2  5759  kmlem4  7993  axpowndlem3  8434  axpownd  8436  hashgt0elex  11629  nmo  23930  elfuns  25672  n0el  26602  pm10.251  27427  pm10.57  27438  2exnaln  27444  elnev  27510  bnj1143  28871
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