Theorem exnal 1828

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 1827. 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 1827	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 357	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃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 207  df-ex 1781

This theorem is referenced by:  alexn  1846  nfnbi  1856  exanali  1860  19.35  1878  19.30  1882  nfeqf2  2377  nabbib  3031  r2exlem  3121  spc3gv  3554  vn0  4290  notzfaus  5296  dtruALT2  5303  dvdemo1  5306  dtruALT  5321  eunex  5323  reusv2lem2  5332  dtru  5374  brprcneu  6807  brprcneuALT  6808  dffv2  6912  zfcndpow  10502  hashfun  14339  nmo  32461  bnj1304  34823  bnj1253  35021  axregs  35137  onvf1odlem4  35142  axrepprim  35738  axunprim  35739  axregprim  35741  axinfprim  35742  axacprim  35743  dftr6  35787  brtxpsd  35928  elfuns  35949  dfrdg4  35985  relowlpssretop  37398  onsupmaxb  43272  clsk3nimkb  44073  expandexn  44322  vk15.4j  44561  vk15.4jVD  44946  alneu  47155