Theorem alnex 1783

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1536  ∃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 210  df-ex 1782

This theorem is referenced by:  nf3  1788  nfntht2  1796  nex  1802  alex  1827  2exnaln  1830  aleximi  1833  19.38  1840  alinexa  1844  alexn  1846  nexdh  1866  19.43  1883  19.43OLD  1884  19.33b  1886  empty  1907  cbvexdvaw  2046  cbvexdw  2348  cbvex  2406  cbvexvOLD  2410  cbvexd  2418  dfmoeu  2594  nexmo  2599  euae  2722  ralnex  3199  cbvrexdva2OLD  3405  vtoclgft  3501  mo2icl  3653  n0el  4275  falseral0  4417  disjsn  4607  axprlem5  5293  dm0rn0  5759  reldm0  5762  iotanul  6302  imadif  6408  dffv2  6733  kmlem4  9564  axpowndlem3  10010  axpownd  10012  hashgt0elex  13758  nelbOLD  30239  nmo  30261  bnj1143  32172  unbdqndv1  33960  bj-nexdh  34074  axc11n11r  34130  bj-hbntbi  34151  bj-modal4e  34162  wl-nfeqfb  34941  wl-sb8et  34954  wl-lem-nexmo  34968  wl-dfrexsb  35016  pm10.251  41064  pm10.57  41075  elnev  41142  spr0nelg  43993  zrninitoringc  44695  alimp-no-surprise  45309