Theorem alnex 1783

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

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 1782

This theorem is referenced by:  nf3  1788  nfntht2  1796  nex  1802  alex  1828  2exnaln  1831  aleximi  1834  19.38  1841  alinexa  1845  alexn  1847  nexdh  1867  19.43  1884  19.43OLD  1885  19.33b  1887  empty  1908  cbvexdvaw  2041  19.8aw  2054  nsb  2112  cbvexdw  2343  cbvexv1  2346  cbvex  2403  cbvexd  2412  dfmoeu  2535  nexmo  2541  euae  2660  ralnex  3063  cbvexeqsetf  3444  mo2icl  3660  n0el  4304  falseral0OLD  4455  disjsn  4655  axpr  5369  axprlem5OLD  5373  axprglem  5378  axprg  5379  dm0rn0  5879  dm0rn0OLD  5880  reldm0  5883  iotanul  6478  imadif  6582  dffv2  6935  kmlem4  10076  axpowndlem3  10522  axpownd  10524  hashgt0elex  14363  zrninitoringc  20653  nmo  32559  bnj1143  34932  axprALT2  35253  axregs  35283  unbdqndv1  36768  bj-exexalal  36871  bj-nexdh  36880  axc11n11r  36980  bj-hbntbi  37001  bj-modal4e  37014  wl-nfeqfb  37861  wl-sb8eft  37876  wl-sb8et  37878  wl-lem-nexmo  37892  wl-issetft  37907  hashnexinj  42567  eu6w  43109  onsupmaxb  43667  pm10.251  44787  pm10.57  44798  elnev  44864  spr0nelg  47936  usgrexmpl12ngric  48514  alimp-no-surprise  50256