Theorem exanali 1822

Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)

Assertion

Ref	Expression
exanali	⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))

Proof of Theorem exanali

Step	Hyp	Ref	Expression
1		annim 395	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
2	1	exbii 1811	. 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓))
3		exnal 1790	. 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
4	2, 3	bitri 267	1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387  ∀wal 1506  ∃wex 1743

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744

This theorem is referenced by:  sbnvOLD  2246  sbnOLD  2463  sbnALT  2523  gencbval  3465  dfss6  3841  nss  3912  nssss  5201  brprcneu  6488  marypha1lem  8690  reclem2pr  10266  dftr6  32543  brsset  32908  dfon3  32911  dffun10  32933  elfuns  32934  ecinn0  35090  ax12indn  35561  expandrexn  40040  vk15.4j  40318  vk15.4jVD  40704