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  2368  cbvexv1  2371  cbvex  2428  cbvexd  2437  dfmoeu  2560  nexmo  2566  euae  2684  ralnex  3088  cbvexeqsetf  3465  mo2icl  3672  n0el  4312  falseral0OLD  4471  disjsn  4672  axpr  5392  axprlem5OLD  5396  axprglem  5401  axprg  5402  dm0rn0  5908  dm0rn0OLD  5909  reldm0  5912  iotanul  6513  imadif  6617  dffv2  6973  kmlem4  10156  axpowndlem3  10608  axpownd  10610  hashgt0elex  14465  zrninitoringc  20838  nmo  32965  bnj1143  35299  axprALT2  35617  axregs  35665  unbdqndv1  37205  bj-exexalal  37307  bj-nexdh  37316  axc11n11r  37416  bj-hbntbi  37437  bj-modal4e  37450  wl-nfeqfb  38299  wl-sb8eft  38314  wl-sb8et  38316  wl-lem-nexmo  38330  wl-issetft  38345  hashnexinj  42994  eu6w  43522  onsupmaxb  44080  pm10.251  45184  pm10.57  45195  elnev  45261  spr0nelg  48376  usgrexmpl12ngric  48954  alimp-no-surprise  50710