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  3567  vn0  4304  notzfaus  5313  dtruALT2  5320  dvdemo1  5323  dtruALT  5338  eunex  5340  reusv2lem2  5349  dtru  5391  dtruOLD  5396  brprcneu  6830  brprcneuALT  6831  dffv2  6938  zfcndpow  10545  hashfun  14378  nmo  32392  bnj1304  34782  bnj1253  34980  onvf1odlem4  35066  axrepprim  35662  axunprim  35663  axregprim  35665  axinfprim  35666  axacprim  35667  dftr6  35711  brtxpsd  35855  elfuns  35876  dfrdg4  35912  relowlpssretop  37325  onsupmaxb  43201  clsk3nimkb  44002  expandexn  44251  vk15.4j  44491  vk15.4jVD  44876  alneu  47098