Theorem alnex 1778

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535  ∃wex 1776

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 1777

This theorem is referenced by:  nf3  1783  nfntht2  1791  nex  1797  alex  1823  2exnaln  1826  aleximi  1829  19.38  1836  alinexa  1840  alexn  1842  nexdh  1863  19.43  1880  19.43OLD  1881  19.33b  1883  empty  1904  cbvexdvaw  2036  19.8aw  2048  nsb  2104  cbvexdw  2340  cbvexv1  2343  cbvex  2402  cbvexd  2411  dfmoeu  2534  nexmo  2539  euae  2658  ralnex  3070  cbvexeqsetf  3493  mo2icl  3723  n0el  4370  falseral0  4522  disjsn  4716  axpr  5433  axprlem5OLD  5436  dm0rn0  5938  reldm0  5941  iotanul  6541  imadif  6652  dffv2  7004  kmlem4  10192  axpowndlem3  10637  axpownd  10639  hashgt0elex  14437  zrninitoringc  20693  nmo  32518  bnj1143  34783  unbdqndv1  36491  bj-nexdh  36611  axc11n11r  36666  bj-hbntbi  36687  bj-modal4e  36698  wl-nfeqfb  37517  wl-sb8eft  37532  wl-sb8et  37534  wl-lem-nexmo  37548  wl-issetft  37563  hashnexinj  42110  eu6w  42663  onsupmaxb  43228  pm10.251  44356  pm10.57  44367  elnev  44434  spr0nelg  47401  usgrexmpl12ngric  47933  alimp-no-surprise  49012