Theorem exanali 1858

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534  ∃wex 1779

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by:  sbnvOLD  2321  sbnOLD  2540  sbnALT  2594  gencbval  3554  dfss6  3960  nss  4032  nssss  5351  brprcneu  6665  marypha1lem  8900  reclem2pr  10473  dftr6  32990  brsset  33354  dfon3  33357  dffun10  33379  elfuns  33380  ecinn0  35611  ax12indn  36083  expandrexn  40633  vk15.4j  40868  vk15.4jVD  41254