Proof of Theorem wl-aleq
Step | Hyp | Ref
| Expression |
1 | | sp 2207 |
. . 3
⊢
(∀𝑥 𝑦 = 𝑧 → 𝑦 = 𝑧) |
2 | | equequ2 2111 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧)) |
3 | 2 | alimi 1887 |
. . . 4
⊢
(∀𝑥 𝑦 = 𝑧 → ∀𝑥(𝑥 = 𝑦 ↔ 𝑥 = 𝑧)) |
4 | | albi 1894 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 ↔ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
5 | 3, 4 | syl 17 |
. . 3
⊢
(∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
6 | 1, 5 | jca 501 |
. 2
⊢
(∀𝑥 𝑦 = 𝑧 → (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) |
7 | | ax7 2101 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
8 | 7 | al2imi 1891 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
9 | 8 | a1dd 50 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))) |
10 | | axc9 2458 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))) |
11 | 9, 10 | bija 369 |
. . 3
⊢
((∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧) → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
12 | 11 | impcom 394 |
. 2
⊢ ((𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) → ∀𝑥 𝑦 = 𝑧) |
13 | 6, 12 | impbii 199 |
1
⊢
(∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) |