Theorem alnex 1785

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

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

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 1784

This theorem is referenced by:  nf3  1790  nfntht2  1798  nex  1804  alex  1829  2exnaln  1832  aleximi  1835  19.38  1842  alinexa  1846  alexn  1848  nexdh  1869  19.43  1886  19.43OLD  1887  19.33b  1889  empty  1910  cbvexdvaw  2043  19.8aw  2054  nsb  2106  cbvexdw  2338  cbvexv1  2341  cbvex  2399  cbvexd  2408  dfmoeu  2536  nexmo  2541  euae  2661  ralnex  3163  vtoclgft  3482  mo2icl  3644  n0el  4292  falseral0  4447  disjsn  4644  axprlem5  5345  dm0rn0  5823  reldm0  5826  iotanul  6396  imadif  6502  dffv2  6845  kmlem4  9840  axpowndlem3  10286  axpownd  10288  hashgt0elex  14044  nelbOLDOLD  30718  nmo  30739  bnj1143  32670  unbdqndv1  34615  bj-nexdh  34736  axc11n11r  34792  bj-hbntbi  34813  bj-modal4e  34824  wl-nfeqfb  35622  wl-sb8et  35635  wl-lem-nexmo  35649  pm10.251  41867  pm10.57  41878  elnev  41945  spr0nelg  44816  zrninitoringc  45517  alimp-no-surprise  46371