Theorem exanali 1860

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 403	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
2	1	exbii 1849	. 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓))
3		exnal 1828	. 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
4	2, 3	bitri 275	1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  gencbval  3499  dfss6  3921  nss  3996  nssss  5401  brprcneu  6822  brprcneuALT  6823  marypha1lem  9334  reclem2pr  10957  dftr6  35894  brsset  36030  dfon3  36033  dffun10  36055  elfuns  36056  ecinn0  38485  ax12indn  39142  expandrexn  44474  vk15.4j  44711  vk15.4jVD  45096