Theorem alnex 1788

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

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545  ∃wex 1786

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 208  df-ex 1787

This theorem is referenced by:  nf3  1793  nfntht2  1801  nex  1807  alex  1833  2exnaln  1836  aleximi  1839  19.38  1846  alinexa  1850  alexn  1852  nexdh  1872  19.43  1889  19.43OLD  1890  19.33b  1892  empty  1913  cbvexdvaw  2046  19.8aw  2059  nsb  2117  cbvexdw  2347  cbvexv1  2350  cbvex  2407  cbvexd  2416  dfmoeu  2539  nexmo  2545  euae  2663  ralnex  3065  cbvexeqsetf  3446  mo2icl  3655  n0el  4292  falseral0OLD  4443  disjsn  4643  axpr  5356  axprlem5OLD  5360  axprglem  5365  axprg  5366  dm0rn0  5866  dm0rn0OLD  5867  reldm0  5870  iotanul  6465  imadif  6569  dffv2  6922  kmlem4  10067  axpowndlem3  10513  axpownd  10515  hashgt0elex  14354  zrninitoringc  20648  nmo  32577  bnj1143  34972  axprALT2  35290  axregs  35320  unbdqndv1  36814  bj-exexalal  36917  bj-nexdh  36926  axc11n11r  37026  bj-hbntbi  37047  bj-modal4e  37060  wl-nfeqfb  37907  wl-sb8eft  37922  wl-sb8et  37924  wl-lem-nexmo  37938  wl-issetft  37953  hashnexinj  42613  eu6w  43126  onsupmaxb  43684  pm10.251  44804  pm10.57  44815  elnev  44881  spr0nelg  47951  usgrexmpl12ngric  48529  alimp-no-surprise  50271