Theorem exanali 1879

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 407	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
2	1	exbii 1868	. 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓))
3		exnal 1847	. 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
4	2, 3	bitri 277	1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1558  ∃wex 1799

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  gencbval  3512  dfss6  3926  nss  4000  nssss  5422  brprcneu  6857  brprcneuALT  6858  marypha1lem  9379  reclem2pr  11006  dftr6  36101  brsset  36237  dfon3  36240  dffun10  36262  elfuns  36263  ecinn0  38852  ax12indn  39567  expandrexn  44867  vk15.4j  45104  vk15.4jVD  45489