Proof of Theorem spsbim
Step | Hyp | Ref
| Expression |
1 | | imim2 49 |
. . . 4
⊢ ((φ → ψ) → ((x = y →
φ) → (x = y →
ψ))) |
2 | 1 | sps 1427 |
. . 3
⊢ (∀x(φ → ψ) → ((x = y →
φ) → (x = y →
ψ))) |
3 | | id 19 |
. . . . . 6
⊢ ((φ → ψ) → (φ → ψ)) |
4 | 3 | anim2d 320 |
. . . . 5
⊢ ((φ → ψ) → ((x = y ∧ φ) →
(x = y
∧ ψ))) |
5 | 4 | alimi 1341 |
. . . 4
⊢ (∀x(φ → ψ) → ∀x((x = y ∧ φ) →
(x = y
∧ ψ))) |
6 | | exim 1487 |
. . . 4
⊢ (∀x((x = y ∧ φ) →
(x = y
∧ ψ))
→ (∃x(x = y ∧ φ) → ∃x(x = y ∧ ψ))) |
7 | 5, 6 | syl 14 |
. . 3
⊢ (∀x(φ → ψ) → (∃x(x = y ∧ φ) →
∃x(x = y ∧ ψ))) |
8 | 2, 7 | anim12d 318 |
. 2
⊢ (∀x(φ → ψ) → (((x = y →
φ) ∧
∃x(x = y ∧ φ)) → ((x = y →
ψ) ∧
∃x(x = y ∧ ψ)))) |
9 | | df-sb 1643 |
. 2
⊢
([y / x]φ ↔
((x = y
→ φ) ∧ ∃x(x = y ∧ φ))) |
10 | | df-sb 1643 |
. 2
⊢
([y / x]ψ ↔
((x = y
→ ψ) ∧ ∃x(x = y ∧ ψ))) |
11 | 8, 9, 10 | 3imtr4g 194 |
1
⊢ (∀x(φ → ψ) → ([y / x]φ → [y / x]ψ)) |