Theorem alnex 1779

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

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

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 1778

This theorem is referenced by:  nf3  1784  nfntht2  1792  nex  1798  alex  1824  2exnaln  1827  aleximi  1830  19.38  1837  alinexa  1841  alexn  1843  nexdh  1864  19.43  1881  19.43OLD  1882  19.33b  1884  empty  1905  cbvexdvaw  2038  19.8aw  2050  nsb  2106  cbvexdw  2345  cbvexv1  2348  cbvex  2407  cbvexd  2416  dfmoeu  2539  nexmo  2544  euae  2663  ralnex  3078  cbvexeqsetf  3503  mo2icl  3736  n0el  4387  falseral0  4539  disjsn  4736  axprlem5  5445  dm0rn0  5949  reldm0  5952  iotanul  6551  imadif  6662  dffv2  7017  kmlem4  10223  axpowndlem3  10668  axpownd  10670  hashgt0elex  14450  zrninitoringc  20698  nmo  32518  bnj1143  34766  unbdqndv1  36474  bj-nexdh  36594  axc11n11r  36649  bj-hbntbi  36670  bj-modal4e  36681  wl-nfeqfb  37490  wl-sb8eft  37505  wl-sb8et  37507  wl-lem-nexmo  37521  wl-issetft  37536  hashnexinj  42085  eu6w  42631  onsupmaxb  43200  pm10.251  44329  pm10.57  44340  elnev  44407  spr0nelg  47350  usgrexmpl12ngric  47853  alimp-no-surprise  48875