Theorem 19.35 1805

Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)

Assertion

Ref	Expression
19.35	⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem 19.35

Step	Hyp	Ref	Expression
1		pm2.27 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	aleximi 1759	. . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
3	2	com12 32	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4		exnal 1754	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5		pm2.21 120	. . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
6	5	eximi 1762	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓))
7	4, 6	sylbir 225	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓))
8		exa1 1765	. . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓))
9	7, 8	ja 173	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
10	3, 9	impbii 199	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1481  ∃wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  19.35i  1806  19.35ri  1807  19.25  1808  19.43  1810  nfimt  1821  nfimdOLDOLD  1824  speimfwALT  1877  19.39  1899  19.24  1900  19.36v  1904  19.37v  1910  19.36  2098  19.37  2100  spimt  2253  grothprim  9656  bj-spimt2  32709  bj-spimtv  32718  bj-snsetex  32951