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

Theorem alnex 1696
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 1695 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 345 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wal 1472  wex 1694
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 195  df-ex 1695
This theorem is referenced by:  nf3  1702  nex  1721  alex  1742  2exnaln  1745  aleximi  1748  19.38  1756  alinexa  1758  alexn  1759  nexdh  1778  19.43  1798  19.43OLD  1799  19.33b  1801  nexdvOLD  1851  cbvexdva  2269  mo2v  2464  ralnex  2974  mo2icl  3351  disjsn  4191  dm0rn0  5250  reldm0  5251  iotanul  5769  imadif  5873  dffv2  6166  kmlem4  8835  axpowndlem3  9277  axpownd  9279  hashgt0elex  13002  nmo  28515  bnj1143  29921  unbdqndv1  31475  bj-nf3  31573  bj-nexdh  31596  bj-modal5e  31631  axc11n11r  31666  bj-hbntbi  31688  bj-modal4e  31698  wl-nfeqfb  32305  wl-sb8et  32316  wl-lem-nexmo  32331  n0el  32967  pm10.251  37384  pm10.57  37395  elnev  37464  falseral0  40113  zrninitoringc  41865  alimp-no-surprise  42299
  Copyright terms: Public domain W3C validator