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

Theorem alnex 1694
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
alnex (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Proof of Theorem alnex
StepHypRef Expression
1 df-ex 1693 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 341 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191  wal 1466  wex 1692
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 192  df-ex 1693
This theorem is referenced by:  nex  1707  alex  1729  2exnaln  1732  aleximi  1735  19.38  1743  alinexa  1744  alexn  1745  nexdh  1756  19.43  1776  19.43OLD  1777  19.33b  1779  nexdv  1813  nf4  2095  mo2v  2360  mo2icl  3241  disjsn  4060  dm0rn0  5100  reldm0  5101  iotanul  5612  imadif  5713  dffv2  6005  kmlem4  8668  axpowndlem3  9109  axpownd  9111  hashgt0elex  12696  nmo  28282  bnj1143  29754  unbdqndv1  31306  bj-nf3  31377  bj-nexdh  31396  bj-modal5e  31431  bj-hbntbi  31483  bj-modal4e  31493  wl-nfeqfb  32101  wl-sb8et  32112  wl-lem-nexmo  32127  n0el  32666  pm10.251  37066  pm10.57  37077  elnev  37146  falseral0  39508  zrninitoringc  41263  alimp-no-surprise  41707
  Copyright terms: Public domain W3C validator