Theorem alnex 1784

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃wex 1782

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 1783

This theorem is referenced by:  nf3  1789  nfntht2  1797  nex  1803  alex  1828  2exnaln  1831  aleximi  1834  19.38  1841  alinexa  1845  alexn  1847  nexdh  1868  19.43  1885  19.43OLD  1886  19.33b  1888  empty  1909  cbvexdvaw  2042  19.8aw  2053  nsb  2104  cbvexdw  2336  cbvexv1  2339  cbvex  2399  cbvexd  2408  dfmoeu  2536  nexmo  2541  euae  2661  ralnex  3167  vtoclgft  3492  mo2icl  3649  n0el  4295  falseral0  4450  disjsn  4647  axprlem5  5350  dm0rn0  5834  reldm0  5837  iotanul  6411  imadif  6518  dffv2  6863  kmlem4  9909  axpowndlem3  10355  axpownd  10357  hashgt0elex  14116  nelbOLDOLD  30817  nmo  30838  bnj1143  32770  unbdqndv1  34688  bj-nexdh  34809  axc11n11r  34865  bj-hbntbi  34886  bj-modal4e  34897  wl-nfeqfb  35695  wl-sb8et  35708  wl-lem-nexmo  35722  pm10.251  41978  pm10.57  41989  elnev  42056  spr0nelg  44928  zrninitoringc  45629  alimp-no-surprise  46485