Theorem exnal 1827

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

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

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

This theorem is referenced by:  alexn  1845  nfnbi  1855  exanali  1859  19.35  1877  19.30  1881  nfeqf2  2375  nabbib  3028  r2exlem  3118  spc3gv  3561  vn0  4298  notzfaus  5305  dtruALT2  5312  dvdemo1  5315  dtruALT  5330  eunex  5332  reusv2lem2  5341  dtru  5383  dtruOLD  5388  brprcneu  6816  brprcneuALT  6817  dffv2  6922  zfcndpow  10529  hashfun  14362  nmo  32452  bnj1304  34788  bnj1253  34986  axregs  35076  onvf1odlem4  35081  axrepprim  35677  axunprim  35678  axregprim  35680  axinfprim  35681  axacprim  35682  dftr6  35726  brtxpsd  35870  elfuns  35891  dfrdg4  35927  relowlpssretop  37340  onsupmaxb  43215  clsk3nimkb  44016  expandexn  44265  vk15.4j  44505  vk15.4jVD  44890  alneu  47112