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 357	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃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 207  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  1865  19.43  1882  19.43OLD  1883  19.33b  1885  empty  1906  cbvexdvaw  2039  19.8aw  2051  nsb  2107  cbvexdw  2337  cbvexv1  2340  cbvex  2397  cbvexd  2406  dfmoeu  2529  nexmo  2534  euae  2653  ralnex  3055  cbvexeqsetf  3462  mo2icl  3685  n0el  4327  falseral0  4479  disjsn  4675  axpr  5382  axprlem5OLD  5385  dm0rn0  5888  reldm0  5891  iotanul  6489  imadif  6600  dffv2  6956  kmlem4  10107  axpowndlem3  10552  axpownd  10554  hashgt0elex  14366  zrninitoringc  20585  nmo  32419  bnj1143  34780  unbdqndv1  36496  bj-nexdh  36616  axc11n11r  36671  bj-hbntbi  36692  bj-modal4e  36703  wl-nfeqfb  37524  wl-sb8eft  37539  wl-sb8et  37541  wl-lem-nexmo  37555  wl-issetft  37570  hashnexinj  42116  eu6w  42664  onsupmaxb  43228  pm10.251  44349  pm10.57  44360  elnev  44427  spr0nelg  47474  usgrexmpl12ngric  48026  alimp-no-surprise  49767