Theorem alnex 1811

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1809

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 1810

This theorem is referenced by:  nf3  1816  nfntht2  1824  nex  1830  alex  1856  2exnaln  1859  aleximi  1862  19.38  1869  alinexa  1873  alexn  1875  nexdh  1895  19.43  1912  19.43OLD  1913  19.33b  1915  empty  1936  cbvexdvaw  2069  19.8aw  2082  nsb  2141  cbvexdw  2371  cbvexv1  2374  cbvex  2431  cbvexd  2440  dfmoeu  2563  nexmo  2569  euae  2687  ralnex  3091  cbvexeqsetf  3470  mo2icl  3677  n0el  4319  falseral0OLD  4476  disjsn  4677  axpr  5398  axprlem5OLD  5402  axprglem  5407  axprg  5408  dm0rn0  5914  dm0rn0OLD  5915  reldm0  5918  iotanul  6516  imadif  6620  dffv2  6976  kmlem4  10133  axpowndlem3  10579  axpownd  10581  hashgt0elex  14433  zrninitoringc  20775  nmo  32836  bnj1143  35178  axprALT2  35503  axregs  35552  unbdqndv1  37097  bj-exexalal  37199  bj-nexdh  37208  axc11n11r  37308  bj-hbntbi  37329  bj-modal4e  37342  wl-nfeqfb  38191  wl-sb8eft  38206  wl-sb8et  38208  wl-lem-nexmo  38222  wl-issetft  38237  hashnexinj  42895  eu6w  43408  onsupmaxb  43966  pm10.251  45070  pm10.57  45081  elnev  45147  spr0nelg  48225  usgrexmpl12ngric  48803  alimp-no-surprise  50559