Theorem exnal 1823

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1534  ∃wex 1775

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

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

This theorem is referenced by:  alexn  1841  nfnbi  1851  exanali  1856  19.35  1874  19.30  1878  nfeqf2  2379  nabbib  3042  r2exlem  3140  spc3gv  3603  vn0  4350  notzfaus  5368  dtruALT2  5375  dvdemo1  5378  dtruALT  5393  eunex  5395  reusv2lem2  5404  dtru  5446  dtruOLD  5451  brprcneu  6896  brprcneuALT  6897  dffv2  7003  zfcndpow  10653  hashfun  14472  nmo  32517  bnj1304  34811  bnj1253  35009  axrepprim  35681  axunprim  35682  axregprim  35684  axinfprim  35685  axacprim  35686  dftr6  35730  brtxpsd  35875  elfuns  35896  dfrdg4  35932  relowlpssretop  37346  onsupmaxb  43227  clsk3nimkb  44029  expandexn  44284  vk15.4j  44525  vk15.4jVD  44911  alneu  47073