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

Theorem alnex 1664
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
alnex  |-  ( A. x  -.  ph  <->  -.  E. x ph )

Proof of Theorem alnex
StepHypRef Expression
1 df-ex 1663 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
21con2bii 334 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188   A.wal 1441   E.wex 1662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-ex 1663
This theorem is referenced by:  nex  1677  alex  1697  2exnaln  1700  aleximi  1703  19.38  1711  alinexa  1712  alexn  1713  nexdh  1724  19.43  1744  19.43OLD  1745  19.33b  1747  nexdv  1781  nf4  2042  mo2v  2305  mo2icl  3216  disjsn  4031  dm0rn0  5050  reldm0  5051  iotanul  5560  imadif  5656  dffv2  5936  kmlem4  8580  axpowndlem3  9021  axpownd  9023  hashgt0elex  12575  nmo  28114  bnj1143  29595  bj-nf3  31186  bj-nexdh  31207  bj-modal5e  31242  bj-hbntbi  31291  bj-modal4e  31301  wl-nfeqfb  31863  wl-sb8et  31874  wl-lem-nexmo  31889  n0el  32427  pm10.251  36703  pm10.57  36714  elnev  36783  falseral0  38980  zrninitoringc  40060  alimp-no-surprise  40507
  Copyright terms: Public domain W3C validator