Step | Hyp | Ref
| Expression |
1 | | alcom 2160 |
. 2
⊢
(∀𝑤∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑)) ↔ ∀𝑥∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑))) |
2 | | 19.21v 1947 |
. . . . . . 7
⊢
(∀𝑥(𝑦 = 𝑤 → 𝜑) ↔ (𝑦 = 𝑤 → ∀𝑥𝜑)) |
3 | 2 | albii 1827 |
. . . . . 6
⊢
(∀𝑦∀𝑥(𝑦 = 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) |
4 | | alcom 2160 |
. . . . . 6
⊢
(∀𝑦∀𝑥(𝑦 = 𝑤 → 𝜑) ↔ ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑)) |
5 | 3, 4 | bitr3i 280 |
. . . . 5
⊢
(∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑) ↔ ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑)) |
6 | 5 | imbi2i 339 |
. . . 4
⊢ ((𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑))) |
7 | 6 | albii 1827 |
. . 3
⊢
(∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑))) |
8 | | df-sb 2071 |
. . 3
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑))) |
9 | | 19.21v 1947 |
. . . 4
⊢
(∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑))) |
10 | 9 | albii 1827 |
. . 3
⊢
(∀𝑤∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥∀𝑦(𝑦 = 𝑤 → 𝜑))) |
11 | 7, 8, 10 | 3bitr4i 306 |
. 2
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑))) |
12 | | df-sb 2071 |
. . 3
⊢ ([𝑧 / 𝑦]𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑))) |
13 | 12 | albii 1827 |
. 2
⊢
(∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜑))) |
14 | 1, 11, 13 | 3bitr4i 306 |
1
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑) |