Proof of Theorem sbal1yz
Step | Hyp | Ref
| Expression |
1 | | dveeq2or 1694 |
. . . . . 6
⊢ (∀x x = z ∨ Ⅎx
y = z) |
2 | | equcom 1590 |
. . . . . . . . 9
⊢ (y = z ↔
z = y) |
3 | 2 | nfbii 1359 |
. . . . . . . 8
⊢
(Ⅎx y = z ↔
Ⅎx z = y) |
4 | | 19.21t 1471 |
. . . . . . . 8
⊢
(Ⅎx z = y →
(∀x(z = y → φ)
↔ (z = y → ∀xφ))) |
5 | 3, 4 | sylbi 114 |
. . . . . . 7
⊢
(Ⅎx y = z →
(∀x(z = y → φ)
↔ (z = y → ∀xφ))) |
6 | 5 | orim2i 677 |
. . . . . 6
⊢ ((∀x x = z ∨ Ⅎx
y = z)
→ (∀x x = z ∨ (∀x(z = y →
φ) ↔ (z = y →
∀xφ)))) |
7 | 1, 6 | ax-mp 7 |
. . . . 5
⊢ (∀x x = z ∨ (∀x(z = y → φ)
↔ (z = y → ∀xφ))) |
8 | 7 | ori 641 |
. . . 4
⊢ (¬
∀x
x = z
→ (∀x(z = y → φ)
↔ (z = y → ∀xφ))) |
9 | 8 | albidv 1702 |
. . 3
⊢ (¬
∀x
x = z
→ (∀y∀x(z = y → φ)
↔ ∀y(z = y → ∀xφ))) |
10 | | alcom 1364 |
. . . 4
⊢ (∀y∀x(z = y →
φ) ↔ ∀x∀y(z = y →
φ)) |
11 | | sb6 1763 |
. . . . . 6
⊢
([z / y]φ ↔
∀y(y = z → φ)) |
12 | 2 | imbi1i 227 |
. . . . . . 7
⊢
((y = z → φ)
↔ (z = y → φ)) |
13 | 12 | albii 1356 |
. . . . . 6
⊢ (∀y(y = z →
φ) ↔ ∀y(z = y →
φ)) |
14 | 11, 13 | bitri 173 |
. . . . 5
⊢
([z / y]φ ↔
∀y(z = y → φ)) |
15 | 14 | albii 1356 |
. . . 4
⊢ (∀x[z / y]φ ↔ ∀x∀y(z = y →
φ)) |
16 | 10, 15 | bitr4i 176 |
. . 3
⊢ (∀y∀x(z = y →
φ) ↔ ∀x[z / y]φ) |
17 | | sb6 1763 |
. . . 4
⊢
([z / y]∀xφ ↔
∀y(y = z → ∀xφ)) |
18 | 2 | imbi1i 227 |
. . . . 5
⊢
((y = z → ∀xφ) ↔ (z = y →
∀xφ)) |
19 | 18 | albii 1356 |
. . . 4
⊢ (∀y(y = z →
∀xφ) ↔ ∀y(z = y →
∀xφ)) |
20 | 17, 19 | bitr2i 174 |
. . 3
⊢ (∀y(z = y →
∀xφ) ↔ [z / y]∀xφ) |
21 | 9, 16, 20 | 3bitr3g 211 |
. 2
⊢ (¬
∀x
x = z
→ (∀x[z / y]φ ↔
[z / y]∀xφ)) |
22 | 21 | bicomd 129 |
1
⊢ (¬
∀x
x = z
→ ([z / y]∀xφ ↔
∀x[z / y]φ)) |