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  2341  cbvexv1  2344  cbvex  2404  cbvexd  2413  dfmoeu  2536  nexmo  2541  euae  2660  ralnex  3063  cbvexeqsetf  3479  mo2icl  3702  n0el  4344  falseral0  4496  disjsn  4692  axpr  5402  axprlem5OLD  5405  dm0rn0  5909  reldm0  5912  iotanul  6514  imadif  6625  dffv2  6979  kmlem4  10173  axpowndlem3  10618  axpownd  10620  hashgt0elex  14424  zrninitoringc  20641  nmo  32476  bnj1143  34826  unbdqndv1  36531  bj-nexdh  36651  axc11n11r  36706  bj-hbntbi  36727  bj-modal4e  36738  wl-nfeqfb  37559  wl-sb8eft  37574  wl-sb8et  37576  wl-lem-nexmo  37590  wl-issetft  37605  hashnexinj  42146  eu6w  42666  onsupmaxb  43230  pm10.251  44351  pm10.57  44362  elnev  44429  spr0nelg  47457  usgrexmpl12ngric  48009  alimp-no-surprise  49612