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  2109  cbvexdw  2339  cbvexv1  2342  cbvex  2399  cbvexd  2408  dfmoeu  2531  nexmo  2536  euae  2655  ralnex  3058  cbvexeqsetf  3451  mo2icl  3668  n0el  4311  falseral0  4463  disjsn  4661  axpr  5363  axprlem5OLD  5366  dm0rn0  5863  dm0rn0OLD  5864  reldm0  5867  iotanul  6461  imadif  6565  dffv2  6917  kmlem4  10045  axpowndlem3  10490  axpownd  10492  hashgt0elex  14308  zrninitoringc  20591  nmo  32469  bnj1143  34802  axregs  35145  unbdqndv1  36550  bj-nexdh  36670  axc11n11r  36725  bj-hbntbi  36746  bj-modal4e  36757  wl-nfeqfb  37578  wl-sb8eft  37593  wl-sb8et  37595  wl-lem-nexmo  37609  wl-issetft  37624  hashnexinj  42169  eu6w  42717  onsupmaxb  43280  pm10.251  44401  pm10.57  44412  elnev  44478  spr0nelg  47515  usgrexmpl12ngric  48077  alimp-no-surprise  49821