Theorem alnex 1775

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1531  ∃wex 1773

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 206  df-ex 1774

This theorem is referenced by:  nf3  1780  nfntht2  1788  nex  1794  alex  1820  2exnaln  1823  aleximi  1826  19.38  1833  alinexa  1837  alexn  1839  nexdh  1860  19.43  1877  19.43OLD  1878  19.33b  1880  empty  1901  cbvexdvaw  2034  19.8aw  2045  nsb  2096  cbvexdw  2330  cbvexv1  2333  cbvex  2393  cbvexd  2402  dfmoeu  2525  nexmo  2530  euae  2650  ralnex  3068  issetft  3485  mo2icl  3709  n0el  4363  falseral0  4521  disjsn  4718  axprlem5  5429  dm0rn0  5929  reldm0  5932  iotanul  6529  imadif  6640  dffv2  6996  kmlem4  10182  axpowndlem3  10628  axpownd  10630  hashgt0elex  14398  zrninitoringc  20614  nmo  32306  bnj1143  34426  unbdqndv1  35988  bj-nexdh  36109  axc11n11r  36165  bj-hbntbi  36186  bj-modal4e  36197  wl-nfeqfb  37008  wl-sb8eft  37023  wl-sb8et  37025  wl-lem-nexmo  37039  wl-issetft  37054  hashnexinj  41603  onsupmaxb  42670  pm10.251  43800  pm10.57  43811  elnev  43878  spr0nelg  46818  alimp-no-surprise  48265