Theorem exanali 1891

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 409	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
2	1	exbii 1880	. 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓))
3		exnal 1859	. 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
4	2, 3	bitri 278	1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  gencbval  3512  dfss6  3903  nss  3977  nssss  5427  brprcneu  6886  brprcneuALT  6887  marypha1lem  9438  reclem2pr  11146  dftr6  36646  brsset  36781  dfon3  36784  dffun10  36806  elfuns  36807  ecinn0  39428  ax12indn  40143  expandrexn  45418  vk15.4j  45653  vk15.4jVD  46038