Step | Hyp | Ref
| Expression |
1 | | dfcleq 2604 |
. . . . 5
⊢ (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) |
2 | 1 | sbbii 1874 |
. . . 4
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ [𝑦 / 𝑥]∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) |
3 | | sbsbc 3406 |
. . . 4
⊢ ([𝑦 / 𝑥]∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) ↔ [𝑦 / 𝑥]∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) |
4 | | sbcal 3452 |
. . . 4
⊢
([𝑦 / 𝑥]∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) ↔ ∀𝑧[𝑦 / 𝑥](𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) |
5 | 2, 3, 4 | 3bitri 285 |
. . 3
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ∀𝑧[𝑦 / 𝑥](𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)) |
6 | | vex 3176 |
. . . . 5
⊢ 𝑦 ∈ V |
7 | | sbcbig 3447 |
. . . . 5
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) ↔ ([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵))) |
8 | 6, 7 | ax-mp 5 |
. . . 4
⊢
([𝑦 / 𝑥](𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) ↔ ([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵)) |
9 | 8 | albii 1737 |
. . 3
⊢
(∀𝑧[𝑦 / 𝑥](𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵) ↔ ∀𝑧([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵)) |
10 | | sbcel2 3941 |
. . . . 5
⊢
([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐴) |
11 | | sbcel2 3941 |
. . . . 5
⊢
([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
12 | 10, 11 | bibi12i 328 |
. . . 4
⊢
(([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵) ↔ (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
13 | 12 | albii 1737 |
. . 3
⊢
(∀𝑧([𝑦 / 𝑥]𝑧 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
14 | 5, 9, 13 | 3bitri 285 |
. 2
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ∀𝑧(𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
15 | | dfcleq 2604 |
. 2
⊢
(⦋𝑦 /
𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵 ↔ ∀𝑧(𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
16 | 14, 15 | bitr4i 266 |
1
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) |