Theorem alnex 1825

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

Syntax hints:  ¬ wn 3   ↔ wb 198  ∀wal 1599  ∃wex 1823

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 199  df-ex 1824

This theorem is referenced by:  nf3  1830  nfntht2  1838  nex  1844  alex  1869  2exnaln  1872  aleximi  1875  19.38  1882  alinexa  1888  alexn  1889  nexdh  1910  19.43  1929  19.43OLD  1930  19.33b  1932  cbvex  2369  cbvexv  2371  cbvexd  2373  cbvexdva  2377  nexmo  2552  nexmoOLD  2553  dfmo  2615  euae  2690  ralnex  3174  mo2icl  3597  n0el  4170  falseral0  4302  disjsn  4478  dm0rn0  5589  reldm0  5590  iotanul  6116  imadif  6220  dffv2  6533  kmlem4  9312  axpowndlem3  9758  axpownd  9760  hashgt0elex  13507  iswspthsnon  27209  nmo  29901  bnj1143  31464  unbdqndv1  33085  bj-nexdh  33189  axc11n11r  33266  bj-hbntbi  33287  bj-modal4e  33297  wl-nfeqfb  33920  wl-sb8et  33932  wl-lem-nexmo  33946  wl-dfrexsb  33989  pm10.251  39525  pm10.57  39536  elnev  39604  spr0nelg  42425  zrninitoringc  43096  alimp-no-surprise  43643