Theorem alnex 1784

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1540  ∃wex 1782

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 206  df-ex 1783

This theorem is referenced by:  nf3  1789  nfntht2  1797  nex  1803  alex  1829  2exnaln  1832  aleximi  1835  19.38  1842  alinexa  1846  alexn  1848  nexdh  1869  19.43  1886  19.43OLD  1887  19.33b  1889  empty  1910  cbvexdvaw  2043  19.8aw  2054  nsb  2105  cbvexdw  2336  cbvexv1  2339  cbvex  2399  cbvexd  2408  dfmoeu  2531  nexmo  2536  euae  2656  ralnex  3073  vtoclgft  3541  mo2icl  3711  n0el  4362  falseral0  4520  disjsn  4716  axprlem5  5426  dm0rn0  5925  reldm0  5928  iotanul  6522  imadif  6633  dffv2  6987  kmlem4  10148  axpowndlem3  10594  axpownd  10596  hashgt0elex  14361  nmo  31730  bnj1143  33801  unbdqndv1  35384  bj-nexdh  35505  axc11n11r  35561  bj-hbntbi  35582  bj-modal4e  35593  wl-nfeqfb  36405  wl-sb8et  36418  wl-lem-nexmo  36432  wl-issetft  36444  onsupmaxb  41988  pm10.251  43119  pm10.57  43130  elnev  43197  spr0nelg  46144  zrninitoringc  46969  alimp-no-surprise  47828