Proof of Theorem sbequiOLD
Step | Hyp | Ref
| Expression |
1 | | equtr 2028 |
. . 3
⊢ (𝑧 = 𝑥 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
2 | | sbequ2 2250 |
. . . 4
⊢ (𝑧 = 𝑥 → ([𝑥 / 𝑧]𝜑 → 𝜑)) |
3 | | sbequ1 2249 |
. . . 4
⊢ (𝑧 = 𝑦 → (𝜑 → [𝑦 / 𝑧]𝜑)) |
4 | 2, 3 | syl9 77 |
. . 3
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) |
5 | 1, 4 | syld 47 |
. 2
⊢ (𝑧 = 𝑥 → (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) |
6 | | ax13 2393 |
. . 3
⊢ (¬
𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
7 | | sp 2182 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → 𝑧 = 𝑥) |
8 | 7 | con3i 157 |
. . . . 5
⊢ (¬
𝑧 = 𝑥 → ¬ ∀𝑧 𝑧 = 𝑥) |
9 | | sb4OLD 2506 |
. . . . 5
⊢ (¬
∀𝑧 𝑧 = 𝑥 → ([𝑥 / 𝑧]𝜑 → ∀𝑧(𝑧 = 𝑥 → 𝜑))) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (¬
𝑧 = 𝑥 → ([𝑥 / 𝑧]𝜑 → ∀𝑧(𝑧 = 𝑥 → 𝜑))) |
11 | | equeuclr 2030 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
12 | 11 | imim1d 82 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 → 𝜑) → (𝑧 = 𝑦 → 𝜑))) |
13 | 12 | al2imi 1816 |
. . . . 5
⊢
(∀𝑧 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑥 → 𝜑) → ∀𝑧(𝑧 = 𝑦 → 𝜑))) |
14 | | sb2 2504 |
. . . . 5
⊢
(∀𝑧(𝑧 = 𝑦 → 𝜑) → [𝑦 / 𝑧]𝜑) |
15 | 13, 14 | syl6 35 |
. . . 4
⊢
(∀𝑧 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑥 → 𝜑) → [𝑦 / 𝑧]𝜑)) |
16 | 10, 15 | syl9 77 |
. . 3
⊢ (¬
𝑧 = 𝑥 → (∀𝑧 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) |
17 | 6, 16 | syld 47 |
. 2
⊢ (¬
𝑧 = 𝑥 → (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) |
18 | 5, 17 | pm2.61i 184 |
1
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) |