Step | Hyp | Ref
| Expression |
1 | | sbcco 3425 |
. . . 4
⊢
([𝐵 / 𝑧][𝑧 / 𝑦]𝜑 ↔ [𝐵 / 𝑦]𝜑) |
2 | 1 | bicomi 213 |
. . 3
⊢
([𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑧][𝑧 / 𝑦]𝜑) |
3 | 2 | sbcbii 3458 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑧][𝑧 / 𝑦]𝜑) |
4 | | sbccom2f.1 |
. . 3
⊢ 𝐴 ∈ V |
5 | 4 | sbccom2 33100 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑧][𝑧 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑧][𝐴 / 𝑥][𝑧 / 𝑦]𝜑) |
6 | | vex 3176 |
. . . . . . 7
⊢ 𝑧 ∈ V |
7 | 6 | sbccom2 33100 |
. . . . . 6
⊢
([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [⦋𝑧 / 𝑦⦌𝐴 / 𝑥][𝑧 / 𝑦]𝜑) |
8 | | sbccom2f.2 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐴 |
9 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → 𝐴 = 𝐴) |
10 | 6, 8, 9 | csbief 3524 |
. . . . . . 7
⊢
⦋𝑧 /
𝑦⦌𝐴 = 𝐴 |
11 | | dfsbcq 3404 |
. . . . . . 7
⊢
(⦋𝑧 /
𝑦⦌𝐴 = 𝐴 → ([⦋𝑧 / 𝑦⦌𝐴 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢
([⦋𝑧 / 𝑦⦌𝐴 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑) |
13 | 7, 12 | bitri 263 |
. . . . 5
⊢
([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑) |
14 | 13 | bicomi 213 |
. . . 4
⊢
([𝐴 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑) |
15 | 14 | sbcbii 3458 |
. . 3
⊢
([⦋𝐴 / 𝑥⦌𝐵 / 𝑧][𝐴 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑧][𝑧 / 𝑦][𝐴 / 𝑥]𝜑) |
16 | | sbcco 3425 |
. . 3
⊢
([⦋𝐴 / 𝑥⦌𝐵 / 𝑧][𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |
17 | 15, 16 | bitri 263 |
. 2
⊢
([⦋𝐴 / 𝑥⦌𝐵 / 𝑧][𝐴 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |
18 | 3, 5, 17 | 3bitri 285 |
1
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |