Theorem alnex 1783

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  nf3  1788  nfntht2  1796  nex  1802  alex  1828  2exnaln  1831  aleximi  1834  19.38  1841  alinexa  1845  alexn  1847  nexdh  1867  19.43  1884  19.43OLD  1885  19.33b  1887  empty  1908  cbvexdvaw  2041  19.8aw  2054  nsb  2112  cbvexdw  2344  cbvexv1  2347  cbvex  2404  cbvexd  2413  dfmoeu  2536  nexmo  2542  euae  2661  ralnex  3064  cbvexeqsetf  3457  mo2icl  3674  n0el  4318  falseral0OLD  4470  disjsn  4670  axpr  5374  axprlem5OLD  5377  axprglem  5382  axprg  5383  dm0rn0  5881  dm0rn0OLD  5882  reldm0  5885  iotanul  6480  imadif  6584  dffv2  6937  kmlem4  10076  axpowndlem3  10522  axpownd  10524  hashgt0elex  14336  zrninitoringc  20621  nmo  32576  bnj1143  34966  axprALT2  35287  axregs  35317  unbdqndv1  36730  bj-exexalal  36831  bj-nexdh  36840  axc11n11r  36928  bj-hbntbi  36949  bj-modal4e  36960  wl-nfeqfb  37791  wl-sb8eft  37806  wl-sb8et  37808  wl-lem-nexmo  37822  wl-issetft  37837  hashnexinj  42498  eu6w  43034  onsupmaxb  43596  pm10.251  44716  pm10.57  44727  elnev  44793  spr0nelg  47836  usgrexmpl12ngric  48398  alimp-no-surprise  50140