Proof of Theorem sbal2
Step | Hyp | Ref
| Expression |
1 | | alcom 1367 |
. . 3
⊢
(∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑)) |
2 | | hbnae 1609 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦) |
3 | | dveeq1 1895 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
4 | 3 | alimi 1344 |
. . . . . 6
⊢
(∀𝑥 ¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
5 | 4 | hbnaes 1611 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
6 | | 19.21ht 1473 |
. . . . 5
⊢
(∀𝑥(𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧) → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
7 | 5, 6 | syl 14 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
8 | 2, 7 | albidh 1369 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
9 | 1, 8 | syl5rbbr 184 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑) ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑))) |
10 | | sb6 1766 |
. 2
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑)) |
11 | | sb6 1766 |
. . 3
⊢ ([𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜑)) |
12 | 11 | albii 1359 |
. 2
⊢
(∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑)) |
13 | 9, 10, 12 | 3bitr4g 212 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |