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  20561  nmo  32392  bnj1143  34753  unbdqndv1  36469  bj-nexdh  36589  axc11n11r  36644  bj-hbntbi  36665  bj-modal4e  36676  wl-nfeqfb  37497  wl-sb8eft  37512  wl-sb8et  37514  wl-lem-nexmo  37528  wl-issetft  37543  hashnexinj  42089  eu6w  42637  onsupmaxb  43201  pm10.251  44322  pm10.57  44333  elnev  44400  spr0nelg  47450  usgrexmpl12ngric  48002  alimp-no-surprise  49743