Proof of Theorem sbequiALT
Step | Hyp | Ref
| Expression |
1 | | equtr 2028 |
. . 3
⊢ (𝑧 = 𝑥 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
2 | | dfsb1.xz |
. . . . 5
⊢ (𝜃 ↔ ((𝑧 = 𝑥 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑥 ∧ 𝜑))) |
3 | 2 | sbequ2ALT 2580 |
. . . 4
⊢ (𝑧 = 𝑥 → (𝜃 → 𝜑)) |
4 | | dfsb1.yz |
. . . . 5
⊢ (𝜏 ↔ ((𝑧 = 𝑦 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝜑))) |
5 | 4 | sbequ1ALT 2579 |
. . . 4
⊢ (𝑧 = 𝑦 → (𝜑 → 𝜏)) |
6 | 3, 5 | syl9 77 |
. . 3
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 → (𝜃 → 𝜏))) |
7 | 1, 6 | syld 47 |
. 2
⊢ (𝑧 = 𝑥 → (𝑥 = 𝑦 → (𝜃 → 𝜏))) |
8 | | ax13 2393 |
. . 3
⊢ (¬
𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
9 | | sp 2182 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → 𝑧 = 𝑥) |
10 | 9 | con3i 157 |
. . . . 5
⊢ (¬
𝑧 = 𝑥 → ¬ ∀𝑧 𝑧 = 𝑥) |
11 | 2 | sb4ALT 2588 |
. . . . 5
⊢ (¬
∀𝑧 𝑧 = 𝑥 → (𝜃 → ∀𝑧(𝑧 = 𝑥 → 𝜑))) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (¬
𝑧 = 𝑥 → (𝜃 → ∀𝑧(𝑧 = 𝑥 → 𝜑))) |
13 | | equeuclr 2030 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
14 | 13 | imim1d 82 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 → 𝜑) → (𝑧 = 𝑦 → 𝜑))) |
15 | 14 | al2imi 1816 |
. . . . 5
⊢
(∀𝑧 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑥 → 𝜑) → ∀𝑧(𝑧 = 𝑦 → 𝜑))) |
16 | 4 | sb2ALT 2587 |
. . . . 5
⊢
(∀𝑧(𝑧 = 𝑦 → 𝜑) → 𝜏) |
17 | 15, 16 | syl6 35 |
. . . 4
⊢
(∀𝑧 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑥 → 𝜑) → 𝜏)) |
18 | 12, 17 | syl9 77 |
. . 3
⊢ (¬
𝑧 = 𝑥 → (∀𝑧 𝑥 = 𝑦 → (𝜃 → 𝜏))) |
19 | 8, 18 | syld 47 |
. 2
⊢ (¬
𝑧 = 𝑥 → (𝑥 = 𝑦 → (𝜃 → 𝜏))) |
20 | 7, 19 | pm2.61i 184 |
1
⊢ (𝑥 = 𝑦 → (𝜃 → 𝜏)) |