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  2340  cbvexv1  2343  cbvex  2403  cbvexd  2412  dfmoeu  2535  nexmo  2540  euae  2659  ralnex  3071  cbvexeqsetf  3494  mo2icl  3719  n0el  4363  falseral0  4515  disjsn  4710  axpr  5426  axprlem5OLD  5429  dm0rn0  5934  reldm0  5937  iotanul  6538  imadif  6649  dffv2  7003  kmlem4  10195  axpowndlem3  10640  axpownd  10642  hashgt0elex  14441  zrninitoringc  20677  nmo  32510  bnj1143  34805  unbdqndv1  36510  bj-nexdh  36630  axc11n11r  36685  bj-hbntbi  36706  bj-modal4e  36717  wl-nfeqfb  37538  wl-sb8eft  37553  wl-sb8et  37555  wl-lem-nexmo  37569  wl-issetft  37584  hashnexinj  42130  eu6w  42691  onsupmaxb  43256  pm10.251  44384  pm10.57  44395  elnev  44462  spr0nelg  47468  usgrexmpl12ngric  48002  alimp-no-surprise  49355