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  3165  vtoclgft  3489  mo2icl  3648  n0el  4295  falseral0  4450  disjsn  4647  axprlem5  5348  dm0rn0  5827  reldm0  5830  iotanul  6404  imadif  6510  dffv2  6855  kmlem4  9919  axpowndlem3  10365  axpownd  10367  hashgt0elex  14126  nelbOLDOLD  30825  nmo  30846  bnj1143  32778  unbdqndv1  34696  bj-nexdh  34817  axc11n11r  34873  bj-hbntbi  34894  bj-modal4e  34905  wl-nfeqfb  35703  wl-sb8et  35716  wl-lem-nexmo  35730  pm10.251  41959  pm10.57  41970  elnev  42037  spr0nelg  44906  zrninitoringc  45607  alimp-no-surprise  46463