Theorem alnex 1808

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1565  ∃wex 1806

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 210  df-ex 1807

This theorem is referenced by:  nf3  1813  nfntht2  1821  nex  1827  alex  1853  2exnaln  1856  aleximi  1859  19.38  1866  alinexa  1870  alexn  1872  nexdh  1892  19.43  1909  19.43OLD  1910  19.33b  1912  empty  1933  cbvexdvaw  2066  19.8aw  2079  nsb  2147  cbvexdw  2377  cbvexv1  2380  cbvex  2437  cbvexd  2446  dfmoeu  2569  nexmo  2575  euae  2693  ralnex  3097  cbvexeqsetf  3478  mo2icl  3686  n0el  4327  falseral0OLD  4481  disjsn  4682  axpr  5399  axprlem5OLD  5403  axprglem  5408  axprg  5409  dm0rn0  5915  dm0rn0OLD  5916  reldm0  5919  iotanul  6517  imadif  6621  dffv2  6977  kmlem4  10136  axpowndlem3  10583  axpownd  10585  hashgt0elex  14436  zrninitoringc  20760  nmo  32776  bnj1143  35122  axprALT2  35444  axregs  35474  unbdqndv1  36985  bj-exexalal  37087  bj-nexdh  37096  axc11n11r  37196  bj-hbntbi  37217  bj-modal4e  37230  wl-nfeqfb  38078  wl-sb8eft  38093  wl-sb8et  38095  wl-lem-nexmo  38109  wl-issetft  38124  hashnexinj  42784  eu6w  43299  onsupmaxb  43857  pm10.251  44961  pm10.57  44972  elnev  45038  spr0nelg  48113  usgrexmpl12ngric  48691  alimp-no-surprise  50443