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  3445  mo2icl  3661  n0el  4305  falseral0OLD  4456  disjsn  4656  axpr  5365  axprlem5OLD  5369  axprglem  5374  axprg  5375  dm0rn0  5874  dm0rn0OLD  5875  reldm0  5878  iotanul  6473  imadif  6577  dffv2  6930  kmlem4  10070  axpowndlem3  10516  axpownd  10518  hashgt0elex  14357  zrninitoringc  20647  nmo  32577  bnj1143  34951  axprALT2  35272  axregs  35302  unbdqndv1  36787  bj-exexalal  36890  bj-nexdh  36899  axc11n11r  36999  bj-hbntbi  37020  bj-modal4e  37033  wl-nfeqfb  37878  wl-sb8eft  37893  wl-sb8et  37895  wl-lem-nexmo  37909  wl-issetft  37924  hashnexinj  42584  eu6w  43126  onsupmaxb  43688  pm10.251  44808  pm10.57  44819  elnev  44885  spr0nelg  47951  usgrexmpl12ngric  48529  alimp-no-surprise  50271