Theorem 19.35 1946

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 1900	. . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
3	2	com12 32	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4		exnal 1895	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5		pm2.21 120	. . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
6	5	eximi 1903	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓))
7	4, 6	sylbir 225	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓))
8		exa1 1906	. . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓))
9	7, 8	ja 173	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
10	3, 9	impbii 199	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

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

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

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

This theorem is referenced by:  19.35i  1947  19.35ri  1948  19.25  1949  19.43  1951  nfimt  1962  nfimdOLDOLD  1965  19.36imv  2014  19.37imv  2016  speimfwALT  2035  19.39  2057  19.24  2058  19.36v  2061  19.37v  2067  19.36  2237  19.37  2239  spimt  2390  grothprim  9840  bj-spimt2  33007  bj-spimtv  33016  bj-snsetex  33249