Theorem alnex 1783

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539  ∃wex 1781

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 1782

This theorem is referenced by:  nf3  1788  nfntht2  1796  nex  1802  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  2335  cbvexv1  2338  cbvex  2397  cbvexd  2406  dfmoeu  2529  nexmo  2534  euae  2654  ralnex  3071  vtoclgft  3510  mo2icl  3675  n0el  4326  falseral0  4482  disjsn  4677  axprlem5  5387  dm0rn0  5885  reldm0  5888  iotanul  6479  imadif  6590  dffv2  6941  kmlem4  10098  axpowndlem3  10544  axpownd  10546  hashgt0elex  14311  nmo  31482  bnj1143  33491  unbdqndv1  35047  bj-nexdh  35168  axc11n11r  35224  bj-hbntbi  35245  bj-modal4e  35256  wl-nfeqfb  36068  wl-sb8et  36081  wl-lem-nexmo  36095  wl-issetft  36107  onsupmaxb  41631  pm10.251  42762  pm10.57  42773  elnev  42840  spr0nelg  45788  zrninitoringc  46489  alimp-no-surprise  47348