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  1917  19.43OLD  1918  19.33b  1920  empty  1941  cbvexdvaw  2074  19.8aw  2087  nsb  2145  cbvexdw  2372  cbvexv1  2375  cbvex  2431  cbvexd  2440  dfmoeu  2563  nexmo  2569  euae  2687  ralnex  3092  cbvexeqsetf  3469  mo2icl  3675  n0el  4315  falseral0OLD  4474  disjsn  4673  axpr  5396  axprglem  5401  axprg  5402  dm0rn0  5918  dm0rn0OLD  5919  reldm0  5922  iotanul  6545  imadif  6654  dffv2  7011  kmlem4  10271  axpowndlem3  10723  axpownd  10725  hashgt0elex  14586  zrninitoringc  20979  nmo  33185  bnj1143  35531  rmo6  35821  axprALT2  35857  axregs  35948  mirimanofffr  36670  unbdqndv1  37589  bj-exexalal  37691  bj-nexdh  37700  axc11n11r  37800  bj-hbntbi  37821  bj-modal4e  37834  wl-nfeqfb  38736  wl-sb8eft  38751  wl-sb8et  38753  wl-lem-nexmo  38767  wl-issetft  38782  hashnexinj  43444  eu6w  43953  onsupmaxb  44502  pm10.251  45605  pm10.57  45616  elnev  45681  spr0nelg  48831  usgrexmpl12ngric  49409  alimp-no-surprise  51305