Theorem alnex 1813

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

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

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 1812

This theorem is used by:  nf3  1818  nfntht2  1826  nex  1832  alex  1858  2exnaln  1861  aleximi  1864  19.38  1871  alinexa  1875  alexn  1877  nexdh  1897  19.43  1914  19.43OLD  1915  19.33b  1917  empty  1938  cbvexdvaw  2071  19.8aw  2084  nsb  2142  cbvexdw  2368  cbvexv1  2371  cbvex  2428  cbvexd  2437  dfmoeu  2560  nexmo  2566  euae  2684  ralnex  3088  cbvexeqsetf  3465  mo2icl  3671  n0el  4311  falseral0OLD  4470  disjsn  4668  axpr  5389  axprglem  5394  axprg  5395  dm0rn0  5907  dm0rn0OLD  5908  reldm0  5911  iotanul  6522  imadif  6629  dffv2  6985  kmlem4  10239  axpowndlem3  10691  axpownd  10693  hashgt0elex  14552  zrninitoringc  20937  nmo  33137  bnj1143  35470  rmo6  35760  axprALT2  35790  axregs  35867  unbdqndv1  37470  bj-exexalal  37572  bj-nexdh  37581  axc11n11r  37681  bj-hbntbi  37702  bj-modal4e  37715  wl-nfeqfb  38577  wl-sb8eft  38592  wl-sb8et  38594  wl-lem-nexmo  38608  wl-issetft  38623  hashnexinj  43287  eu6w  43796  onsupmaxb  44350  pm10.251  45453  pm10.57  45464  elnev  45529  spr0nelg  48666  usgrexmpl12ngric  49244  alimp-no-surprise  51060