Theorem alnex 1814

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nf3  1819  nfntht2  1827  nex  1833  alex  1859  2exnaln  1862  aleximi  1865  19.38  1872  alinexa  1876  alexn  1878  nexdh  1898  19.43  1915  19.43OLD  1916  19.33b  1918  empty  1939  cbvexdvaw  2072  19.8aw  2085  nsb  2144  cbvexdw  2373  cbvexv1  2376  cbvex  2433  cbvexd  2442  dfmoeu  2565  nexmo  2571  euae  2689  ralnex  3093  cbvexeqsetf  3472  mo2icl  3679  n0el  4319  falseral0OLD  4478  disjsn  4679  axpr  5400  axprlem5OLD  5404  axprglem  5409  axprg  5410  dm0rn0  5916  dm0rn0OLD  5917  reldm0  5920  iotanul  6520  imadif  6624  dffv2  6980  kmlem4  10153  axpowndlem3  10599  axpownd  10601  hashgt0elex  14455  zrninitoringc  20825  nmo  32907  bnj1143  35243  axprALT2  35561  axregs  35609  unbdqndv1  37154  bj-exexalal  37256  bj-nexdh  37265  axc11n11r  37365  bj-hbntbi  37386  bj-modal4e  37399  wl-nfeqfb  38248  wl-sb8eft  38263  wl-sb8et  38265  wl-lem-nexmo  38279  wl-issetft  38294  hashnexinj  42953  eu6w  43466  onsupmaxb  44024  pm10.251  45128  pm10.57  45139  elnev  45205  spr0nelg  48283  usgrexmpl12ngric  48861  alimp-no-surprise  50616