Theorem alnex 1780

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1537  ∃wex 1778

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 207  df-ex 1779

This theorem is referenced by:  nf3  1785  nfntht2  1793  nex  1799  alex  1825  2exnaln  1828  aleximi  1831  19.38  1838  alinexa  1842  alexn  1844  nexdh  1864  19.43  1881  19.43OLD  1882  19.33b  1884  empty  1905  cbvexdvaw  2037  19.8aw  2049  nsb  2105  cbvexdw  2339  cbvexv1  2342  cbvex  2402  cbvexd  2411  dfmoeu  2534  nexmo  2539  euae  2658  ralnex  3061  cbvexeqsetf  3478  mo2icl  3702  n0el  4344  falseral0  4496  disjsn  4691  axpr  5407  axprlem5OLD  5410  dm0rn0  5915  reldm0  5918  iotanul  6519  imadif  6630  dffv2  6984  kmlem4  10176  axpowndlem3  10621  axpownd  10623  hashgt0elex  14422  zrninitoringc  20644  nmo  32437  bnj1143  34763  unbdqndv1  36468  bj-nexdh  36588  axc11n11r  36643  bj-hbntbi  36664  bj-modal4e  36675  wl-nfeqfb  37496  wl-sb8eft  37511  wl-sb8et  37513  wl-lem-nexmo  37527  wl-issetft  37542  hashnexinj  42088  eu6w  42649  onsupmaxb  43214  pm10.251  44336  pm10.57  44347  elnev  44414  spr0nelg  47421  usgrexmpl12ngric  47955  alimp-no-surprise  49308