Theorem exnal 1822

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1532  ∃wex 1774

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

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  alexn  1840  nfnbi  1850  exanali  1855  19.35  1873  19.30  1877  nfeqf2  2371  nabbib  3035  r2exlem  3133  spc3gv  3590  vn0  4341  notzfaus  5367  dtruALT2  5374  dvdemo1  5377  dtruALT  5392  eunex  5394  reusv2lem2  5403  dtru  5442  dtruOLD  5447  brprcneu  6891  brprcneuALT  6892  dffv2  6997  zfcndpow  10659  hashfun  14454  nmo  32418  bnj1304  34664  bnj1253  34862  axrepprim  35524  axunprim  35525  axregprim  35527  axinfprim  35528  axacprim  35529  dftr6  35573  brtxpsd  35718  elfuns  35739  dfrdg4  35775  relowlpssretop  37071  onsupmaxb  42904  clsk3nimkb  43707  expandexn  43963  vk15.4j  44204  vk15.4jVD  44590  alneu  46737

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »