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

Theorem alnex 1854
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 1853 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 346 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1629  wex 1852
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 197  df-ex 1853
This theorem is referenced by:  nf3  1860  nex  1879  alex  1901  2exnaln  1904  aleximi  1907  19.38  1914  alinexa  1920  alexn  1921  nexdh  1943  19.43  1962  19.43OLD  1963  19.33b  1965  nexdvOLD  2017  cbvex  2433  cbvexv  2435  cbvexd  2437  cbvexdva  2441  mo2v  2625  ralnex  3141  mo2icl  3538  n0el  4088  falseral0  4221  disjsn  4384  dm0rn0  5481  reldm0  5482  iotanul  6010  imadif  6114  dffv2  6414  kmlem4  9178  axpowndlem3  9624  axpownd  9626  hashgt0elex  13392  iswspthsnon  26987  nmo  29666  bnj1143  31200  unbdqndv1  32837  bj-nexdh  32944  axc11n11r  33011  bj-hbntbi  33033  bj-modal4e  33043  wl-nfeqfb  33659  wl-sb8et  33670  wl-lem-nexmo  33684  pm10.251  39086  pm10.57  39097  elnev  39166  spr0nelg  42255  zrninitoringc  42600  alimp-no-surprise  43059
  Copyright terms: Public domain W3C validator