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  6518  imadif  6624  dffv2  6980  kmlem4  10232  axpowndlem3  10684  axpownd  10686  hashgt0elex  14545  zrninitoringc  20928  nmo  33086  bnj1143  35420  axprALT2  35734  axregs  35807  unbdqndv1  37374  bj-exexalal  37476  bj-nexdh  37485  axc11n11r  37585  bj-hbntbi  37606  bj-modal4e  37619  wl-nfeqfb  38468  wl-sb8eft  38483  wl-sb8et  38485  wl-lem-nexmo  38499  wl-issetft  38514  hashnexinj  43178  eu6w  43687  onsupmaxb  44240  pm10.251  45343  pm10.57  45354  elnev  45420  spr0nelg  48557  usgrexmpl12ngric  49135  alimp-no-surprise  50876