Theorem exnal 1827

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1535  ∃wex 1780

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

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

This theorem is referenced by:  alexn  1845  exanali  1859  19.35  1878  19.30  1882  nfeqf2  2395  nabbi  3121  r2exlem  3302  spc3gv  3605  notzfaus  5262  notzfausOLD  5263  dtru  5271  dvdemo1  5274  dtruALT  5289  eunex  5291  reusv2lem2  5300  dtruALT2  5336  brprcneu  6662  dffv2  6756  zfcndpow  10038  hashfun  13799  nmo  30254  bnj1304  32091  bnj1253  32289  axrepprim  32928  axunprim  32929  axregprim  32931  axinfprim  32932  axacprim  32933  dftr6  32986  brtxpsd  33355  elfuns  33376  dfrdg4  33412  bj-dtru  34139  relowlpssretop  34648  sn-dtru  39131  clsk3nimkb  40410  expandexn  40645  vk15.4j  40882  vk15.4jVD  41268  alneu  43343