Theorem exnal 1846

Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1800. See also the dual pair df-ex 1799 / alex 1845. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
exnal	⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1845	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 359	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  alexn  1864  nfnbi  1874  exanali  1878  19.35  1896  19.30  1900  nfeqf2  2407  nabbib  3059  r2exlem  3150  spc3gv  3562  vn0  4295  notzfaus  5317  dtruALT2  5324  dvdemo1  5327  dtruALT  5342  eunex  5344  reusv2lem2  5353  dtru  5401  brprcneu  6852  brprcneuALT  6853  dffv2  6957  zfcndpow  10568  hashfun  14444  nmo  32648  bnj1304  35075  bnj1253  35273  axregs  35396  onvf1odlem4  35410  axrepprim  36013  axunprim  36014  axregprim  36016  axinfprim  36017  axacprim  36018  dftr6  36062  brtxpsd  36203  elfuns  36224  dfrdg4  36262  bj-cbvaw  37074  relowlpssretop  37819  onsupmaxb  43777  clsk3nimkb  44577  expandexn  44826  vk15.4j  45065  vk15.4jVD  45450  alneu  47679