Theorem alnex 1782

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃wex 1780

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 1781

This theorem is referenced by:  nf3  1787  nfntht2  1795  nex  1801  alex  1827  2exnaln  1830  aleximi  1833  19.38  1840  alinexa  1844  alexn  1846  nexdh  1866  19.43  1883  19.43OLD  1884  19.33b  1886  empty  1907  cbvexdvaw  2040  19.8aw  2053  nsb  2111  cbvexdw  2341  cbvexv1  2344  cbvex  2401  cbvexd  2410  dfmoeu  2533  nexmo  2539  euae  2658  ralnex  3060  cbvexeqsetf  3453  mo2icl  3670  n0el  4314  falseral0OLD  4466  disjsn  4666  axpr  5370  axprlem5OLD  5373  dm0rn0  5871  dm0rn0OLD  5872  reldm0  5875  iotanul  6470  imadif  6574  dffv2  6927  kmlem4  10062  axpowndlem3  10508  axpownd  10510  hashgt0elex  14322  zrninitoringc  20607  nmo  32513  bnj1143  34895  axregs  35244  unbdqndv1  36651  bj-nexdh  36771  axc11n11r  36827  bj-hbntbi  36848  bj-modal4e  36859  wl-nfeqfb  37680  wl-sb8eft  37695  wl-sb8et  37697  wl-lem-nexmo  37711  wl-issetft  37726  hashnexinj  42321  eu6w  42861  onsupmaxb  43423  pm10.251  44543  pm10.57  44554  elnev  44620  spr0nelg  47664  usgrexmpl12ngric  48226  alimp-no-surprise  49968