Theorem exnal 1829

Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1783. See also the dual pair df-ex 1782 / alex 1828. 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 1828	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 357	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  alexn  1847  nfnbi  1857  exanali  1861  19.35  1879  19.30  1883  nfeqf2  2381  nabbib  3035  r2exlem  3126  spc3gv  3546  vn0  4285  notzfaus  5305  dtruALT2  5312  dvdemo1  5315  dtruALT  5330  eunex  5332  reusv2lem2  5341  dtru  5389  brprcneu  6830  brprcneuALT  6831  dffv2  6935  zfcndpow  10539  hashfun  14399  nmo  32559  bnj1304  34961  bnj1253  35159  axregs  35283  onvf1odlem4  35288  axrepprim  35884  axunprim  35885  axregprim  35887  axinfprim  35888  axacprim  35889  dftr6  35933  brtxpsd  36074  elfuns  36095  dfrdg4  36133  bj-cbvaw  36935  relowlpssretop  37680  onsupmaxb  43667  clsk3nimkb  44467  expandexn  44716  vk15.4j  44955  vk15.4jVD  45340  alneu  47572