Theorem alnex 1801

Description: Universal quantification of negation is equivalent to negation of existential quantification. Dual of exnal 1847 (but does not depend on ax-4 1829 contrary to it). See also the dual pair df-ex 1800 / alex 1846. Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
alnex	⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 1800	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2	1	con2bii 359	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1558  ∃wex 1799

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 209  df-ex 1800

This theorem is referenced by:  nf3  1806  nfntht2  1814  nex  1820  alex  1846  2exnaln  1849  aleximi  1852  19.38  1859  alinexa  1863  alexn  1865  nexdh  1885  19.43  1902  19.43OLD  1903  19.33b  1905  empty  1926  cbvexdvaw  2059  19.8aw  2072  nsb  2140  cbvexdw  2370  cbvexv1  2373  cbvex  2430  cbvexd  2439  dfmoeu  2562  nexmo  2568  euae  2686  ralnex  3088  cbvexeqsetf  3469  mo2icl  3677  n0el  4317  falseral0OLD  4469  disjsn  4670  axpr  5384  axprlem5OLD  5388  axprglem  5393  axprg  5394  dm0rn0  5900  dm0rn0OLD  5901  reldm0  5904  iotanul  6501  imadif  6605  dffv2  6962  kmlem4  10110  axpowndlem3  10557  axpownd  10559  hashgt0elex  14414  zrninitoringc  20722  nmo  32686  bnj1143  35082  axprALT2  35402  axregs  35432  unbdqndv1  36943  bj-exexalal  37046  bj-nexdh  37055  axc11n11r  37155  bj-hbntbi  37176  bj-modal4e  37189  wl-nfeqfb  38036  wl-sb8eft  38051  wl-sb8et  38053  wl-lem-nexmo  38067  wl-issetft  38082  hashnexinj  42742  eu6w  43255  onsupmaxb  43813  pm10.251  44933  pm10.57  44944  elnev  45010  spr0nelg  48079  usgrexmpl12ngric  48657  alimp-no-surprise  50399