Proof of Theorem sbalyz
Step | Hyp | Ref
| Expression |
1 | | ax-ial 1358 |
. . . 4
⊢ (∀xφ → ∀x∀xφ) |
2 | 1 | hbsbv 1683 |
. . 3
⊢ ([z / y]∀xφ → ∀x[z / y]∀xφ) |
3 | | ax-4 1333 |
. . . . 5
⊢ (∀xφ → φ) |
4 | 3 | sbimi 1526 |
. . . 4
⊢ ([z / y]∀xφ → [z / y]φ) |
5 | 4 | alimi 1275 |
. . 3
⊢ (∀x[z / y]∀xφ → ∀x[z / y]φ) |
6 | 2, 5 | syl 13 |
. 2
⊢ ([z / y]∀xφ → ∀x[z / y]φ) |
7 | | sb6 1637 |
. . . . 5
⊢ ([z / y]φ ↔ ∀y(y = z →
φ)) |
8 | 7 | albii 1290 |
. . . 4
⊢ (∀x[z / y]φ ↔ ∀x∀y(y = z →
φ)) |
9 | | alcom 1297 |
. . . 4
⊢ (∀x∀y(y = z →
φ) ↔ ∀y∀x(y = z →
φ)) |
10 | 8, 9 | bitri 171 |
. . 3
⊢ (∀x[z / y]φ ↔ ∀y∀x(y = z →
φ)) |
11 | | ax-17 1349 |
. . . . . 6
⊢ (y = z →
∀x
y = z) |
12 | | alim 1277 |
. . . . . 6
⊢ (∀x(y = z →
φ) → (∀x y = z →
∀xφ)) |
13 | 11, 12 | syl5 26 |
. . . . 5
⊢ (∀x(y = z →
φ) → (y = z →
∀xφ)) |
14 | 13 | alimi 1275 |
. . . 4
⊢ (∀y∀x(y = z →
φ) → ∀y(y = z →
∀xφ)) |
15 | | sb2 1529 |
. . . 4
⊢ (∀y(y = z →
∀xφ) → [z / y]∀xφ) |
16 | 14, 15 | syl 13 |
. . 3
⊢ (∀y∀x(y = z →
φ) → [z / y]∀xφ) |
17 | 10, 16 | sylbi 112 |
. 2
⊢ (∀x[z / y]φ → [z / y]∀xφ) |
18 | 6, 17 | impbii 115 |
1
⊢ ([z / y]∀xφ ↔ ∀x[z / y]φ) |