Proof of Theorem bj-ssbcom3lem
Step | Hyp | Ref
| Expression |
1 | | equequ2 1940 |
. . . . . . 7
⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) |
2 | 1 | imbi1d 330 |
. . . . . 6
⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
3 | 2 | pm5.74i 259 |
. . . . 5
⊢ ((𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albii 1737 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
5 | | 19.21v 1855 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
6 | | 19.21v 1855 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑)) ↔ (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
7 | 4, 5, 6 | 3bitr3i 289 |
. . 3
⊢ ((𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
8 | 7 | albii 1737 |
. 2
⊢
(∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
9 | | bj-ssb1 31822 |
. . . 4
⊢ ([𝑦/𝑥]b𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
10 | 9 | bj-ssbbii 31813 |
. . 3
⊢ ([𝑡/𝑦]b[𝑦/𝑥]b𝜑 ↔ [𝑡/𝑦]b∀𝑥(𝑥 = 𝑦 → 𝜑)) |
11 | | bj-ssb1 31822 |
. . 3
⊢ ([𝑡/𝑦]b∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
12 | 10, 11 | bitri 263 |
. 2
⊢ ([𝑡/𝑦]b[𝑦/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
13 | | bj-ssb1 31822 |
. . . 4
⊢ ([𝑡/𝑥]b𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
14 | 13 | bj-ssbbii 31813 |
. . 3
⊢ ([𝑡/𝑦]b[𝑡/𝑥]b𝜑 ↔ [𝑡/𝑦]b∀𝑥(𝑥 = 𝑡 → 𝜑)) |
15 | | bj-ssb1 31822 |
. . 3
⊢ ([𝑡/𝑦]b∀𝑥(𝑥 = 𝑡 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
16 | 14, 15 | bitri 263 |
. 2
⊢ ([𝑡/𝑦]b[𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
17 | 8, 12, 16 | 3bitr4i 291 |
1
⊢ ([𝑡/𝑦]b[𝑦/𝑥]b𝜑 ↔ [𝑡/𝑦]b[𝑡/𝑥]b𝜑) |