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  2376  nabbib  3029  r2exlem  3123  spc3gv  3573  vn0  4311  notzfaus  5321  dtruALT2  5328  dvdemo1  5331  dtruALT  5346  eunex  5348  reusv2lem2  5357  dtru  5399  dtruOLD  5404  brprcneu  6851  brprcneuALT  6852  dffv2  6959  zfcndpow  10576  hashfun  14409  nmo  32426  bnj1304  34816  bnj1253  35014  onvf1odlem4  35100  axrepprim  35696  axunprim  35697  axregprim  35699  axinfprim  35700  axacprim  35701  dftr6  35745  brtxpsd  35889  elfuns  35910  dfrdg4  35946  relowlpssretop  37359  onsupmaxb  43235  clsk3nimkb  44036  expandexn  44285  vk15.4j  44525  vk15.4jVD  44910  alneu  47129