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

Theorem alnex 1703
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 1702 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
21con2bii 347 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1478  wex 1701
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 1702
This theorem is referenced by:  nf3  1709  nex  1728  alex  1750  2exnaln  1753  aleximi  1756  19.38  1763  alinexa  1767  alexn  1768  nexdh  1789  19.43  1807  19.43OLD  1808  19.33b  1810  nexdvOLD  1862  cbvexdva  2282  mo2v  2476  ralnex  2988  mo2icl  3372  falseral0  4059  disjsn  4223  dm0rn0  5312  reldm0  5313  iotanul  5835  imadif  5941  dffv2  6238  kmlem4  8935  axpowndlem3  9381  axpownd  9383  hashgt0elex  13145  nmo  29214  bnj1143  30622  unbdqndv1  32194  bj-nexdh  32301  bj-modal5e  32331  axc11n11r  32368  bj-hbntbi  32390  bj-modal4e  32400  wl-nfeqfb  32994  wl-sb8et  33005  wl-lem-nexmo  33020  n0el  33665  pm10.251  38080  pm10.57  38091  elnev  38160  spr0nelg  41044  zrninitoringc  41389  alimp-no-surprise  41860
  Copyright terms: Public domain W3C validator