Theorem 19.35 1957

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 1907	. . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
3	2	com12 32	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4		exnal 1902	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5		pm2.21 121	. . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
6	5	eximi 1910	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓))
7	4, 6	sylbir 225	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓))
8		exa1 1913	. . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓))
9	7, 8	ja 174	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
10	3, 9	impbii 199	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

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

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

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

This theorem is referenced by:  19.35i  1958  19.35ri  1959  19.25  1960  19.43  1962  nfimd  1973  nfimdOLDOLD  1975  19.36imv  2025  19.37imv  2027  speimfwALT  2046  19.39  2068  19.24  2069  19.36v  2072  19.37v  2078  19.36  2254  19.37  2256  spimt  2415  grothprim  9856  bj-nfimt  32947  bj-spimt2  33039  bj-spimtv  33048  bj-snsetex  33275