Theorem alnex 1781

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

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 1780

This theorem is referenced by:  nf3  1786  nfntht2  1794  nex  1800  alex  1826  2exnaln  1829  aleximi  1832  19.38  1839  alinexa  1843  alexn  1845  nexdh  1865  19.43  1882  19.43OLD  1883  19.33b  1885  empty  1906  cbvexdvaw  2039  19.8aw  2051  nsb  2107  cbvexdw  2337  cbvexv1  2340  cbvex  2397  cbvexd  2406  dfmoeu  2529  nexmo  2534  euae  2653  ralnex  3055  cbvexeqsetf  3451  mo2icl  3674  n0el  4315  falseral0  4467  disjsn  4663  axpr  5366  axprlem5OLD  5369  dm0rn0  5867  reldm0  5870  iotanul  6462  imadif  6566  dffv2  6918  kmlem4  10048  axpowndlem3  10493  axpownd  10495  hashgt0elex  14308  zrninitoringc  20561  nmo  32434  bnj1143  34757  axregs  35074  unbdqndv1  36482  bj-nexdh  36602  axc11n11r  36657  bj-hbntbi  36678  bj-modal4e  36689  wl-nfeqfb  37510  wl-sb8eft  37525  wl-sb8et  37527  wl-lem-nexmo  37541  wl-issetft  37556  hashnexinj  42101  eu6w  42649  onsupmaxb  43212  pm10.251  44333  pm10.57  44344  elnev  44411  spr0nelg  47460  usgrexmpl12ngric  48022  alimp-no-surprise  49766