Theorem alnex 1781

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃wex 1779

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 1780

This theorem is referenced by:  nf3  1786  nfntht2  1794  nex  1800  alex  1826  2exnaln  1829  aleximi  1832  19.38  1839  alinexa  1843  alexn  1845  nexdh  1866  19.43  1883  19.43OLD  1884  19.33b  1886  empty  1907  cbvexdvaw  2040  19.8aw  2051  nsb  2102  cbvexdw  2333  cbvexv1  2336  cbvex  2396  cbvexd  2405  dfmoeu  2528  nexmo  2533  euae  2653  ralnex  3070  issetft  3486  mo2icl  3711  n0el  4362  falseral0  4520  disjsn  4716  axprlem5  5426  dm0rn0  5925  reldm0  5928  iotanul  6522  imadif  6633  dffv2  6987  kmlem4  10152  axpowndlem3  10598  axpownd  10600  hashgt0elex  14367  nmo  31995  bnj1143  34097  unbdqndv1  35689  bj-nexdh  35810  axc11n11r  35866  bj-hbntbi  35887  bj-modal4e  35898  wl-nfeqfb  36710  wl-sb8et  36723  wl-lem-nexmo  36737  wl-issetft  36749  onsupmaxb  42292  pm10.251  43423  pm10.57  43434  elnev  43501  spr0nelg  46444  zrninitoringc  47059  alimp-no-surprise  47917