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  3459  mo2icl  3682  n0el  4323  falseral0  4475  disjsn  4671  axpr  5377  axprlem5OLD  5380  dm0rn0  5878  reldm0  5881  iotanul  6477  imadif  6584  dffv2  6938  kmlem4  10083  axpowndlem3  10528  axpownd  10530  hashgt0elex  14342  zrninitoringc  20596  nmo  32469  bnj1143  34773  unbdqndv1  36489  bj-nexdh  36609  axc11n11r  36664  bj-hbntbi  36685  bj-modal4e  36696  wl-nfeqfb  37517  wl-sb8eft  37532  wl-sb8et  37534  wl-lem-nexmo  37548  wl-issetft  37563  hashnexinj  42109  eu6w  42657  onsupmaxb  43221  pm10.251  44342  pm10.57  44353  elnev  44420  spr0nelg  47470  usgrexmpl12ngric  48022  alimp-no-surprise  49763