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  3122  spc3gv  3570  vn0  4308  notzfaus  5318  dtruALT2  5325  dvdemo1  5328  dtruALT  5343  eunex  5345  reusv2lem2  5354  dtru  5396  dtruOLD  5401  brprcneu  6848  brprcneuALT  6849  dffv2  6956  zfcndpow  10569  hashfun  14402  nmo  32419  bnj1304  34809  bnj1253  35007  onvf1odlem4  35093  axrepprim  35689  axunprim  35690  axregprim  35692  axinfprim  35693  axacprim  35694  dftr6  35738  brtxpsd  35882  elfuns  35903  dfrdg4  35939  relowlpssretop  37352  onsupmaxb  43228  clsk3nimkb  44029  expandexn  44278  vk15.4j  44518  vk15.4jVD  44903  alneu  47125