Theorem alnex 1782

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃wex 1780

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 1781

This theorem is referenced by:  nf3  1787  nfntht2  1795  nex  1801  alex  1827  2exnaln  1830  aleximi  1833  19.38  1840  alinexa  1844  alexn  1846  nexdh  1866  19.43  1883  19.43OLD  1884  19.33b  1886  empty  1907  cbvexdvaw  2040  19.8aw  2053  nsb  2111  cbvexdw  2343  cbvexv1  2346  cbvex  2403  cbvexd  2412  dfmoeu  2535  nexmo  2541  euae  2660  ralnex  3062  cbvexeqsetf  3455  mo2icl  3672  n0el  4316  falseral0OLD  4468  disjsn  4668  axpr  5372  axprlem5OLD  5375  dm0rn0  5873  dm0rn0OLD  5874  reldm0  5877  iotanul  6472  imadif  6576  dffv2  6929  kmlem4  10064  axpowndlem3  10510  axpownd  10512  hashgt0elex  14324  zrninitoringc  20609  nmo  32564  bnj1143  34946  axregs  35295  unbdqndv1  36708  bj-nexdh  36828  axc11n11r  36884  bj-hbntbi  36905  bj-modal4e  36916  wl-nfeqfb  37741  wl-sb8eft  37756  wl-sb8et  37758  wl-lem-nexmo  37772  wl-issetft  37787  hashnexinj  42382  eu6w  42919  onsupmaxb  43481  pm10.251  44601  pm10.57  44612  elnev  44678  spr0nelg  47722  usgrexmpl12ngric  48284  alimp-no-surprise  50026