Theorem alnex 1814

Description: Universal quantification of negation is equivalent to negation of existential quantification. Dual of exnal 1860 (but does not depend on ax-4 1842 contrary to it). See also the dual pair df-ex 1813 / alex 1859. 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 1813	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2	1	con2bii 360	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nf3  1819  nfntht2  1827  nex  1833  alex  1859  2exnaln  1862  aleximi  1865  19.38  1872  alinexa  1876  alexn  1878  nexdh  1898  19.43  1915  19.43OLD  1916  19.33b  1918  empty  1939  cbvexdvaw  2072  19.8aw  2085  nsb  2143  cbvexdw  2369  cbvexv1  2372  cbvex  2429  cbvexd  2438  dfmoeu  2561  nexmo  2567  euae  2685  ralnex  3089  cbvexeqsetf  3466  mo2icl  3672  n0el  4312  falseral0OLD  4471  disjsn  4672  axpr  5389  axprglem  5394  axprg  5395  dm0rn0  5906  dm0rn0OLD  5907  reldm0  5910  iotanul  6517  imadif  6622  dffv2  6978  kmlem4  10225  axpowndlem3  10677  axpownd  10679  hashgt0elex  14538  zrninitoringc  20921  nmo  33079  bnj1143  35413  axprALT2  35723  axregs  35790  unbdqndv1  37354  bj-exexalal  37456  bj-nexdh  37465  axc11n11r  37565  bj-hbntbi  37586  bj-modal4e  37599  wl-nfeqfb  38448  wl-sb8eft  38463  wl-sb8et  38465  wl-lem-nexmo  38479  wl-issetft  38494  hashnexinj  43158  eu6w  43667  onsupmaxb  44225  pm10.251  45329  pm10.57  45340  elnev  45406  spr0nelg  48527  usgrexmpl12ngric  49105  alimp-no-surprise  50846