Step | Hyp | Ref
| Expression |
1 | | df-csb 3028 |
. . . . . 6
⊢
⦋𝑦 /
𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} |
2 | 1 | abeq2i 2265 |
. . . . 5
⊢ (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵) |
3 | 2 | sbcbii 2992 |
. . . 4
⊢
([𝐴 / 𝑦]𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ [𝐴 / 𝑦][𝑦 / 𝑥]𝑧 ∈ 𝐵) |
4 | | nfv 1505 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∀𝑥(𝑥 = 𝑤 → 𝑧 ∈ 𝐵) |
5 | | equequ2 1690 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑤)) |
6 | 5 | imbi1d 230 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝐵) ↔ (𝑥 = 𝑤 → 𝑧 ∈ 𝐵))) |
7 | 6 | albidv 1801 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝑤 → 𝑧 ∈ 𝐵))) |
8 | 4, 7 | sbiev 1769 |
. . . . . . . . 9
⊢ ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝑤 → 𝑧 ∈ 𝐵)) |
9 | | sb6 1863 |
. . . . . . . . 9
⊢ ([𝑤 / 𝑥]𝑧 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝑤 → 𝑧 ∈ 𝐵)) |
10 | 8, 9 | bitr4i 186 |
. . . . . . . 8
⊢ ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵) ↔ [𝑤 / 𝑥]𝑧 ∈ 𝐵) |
11 | | df-clab 2141 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)} ↔ [𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)) |
12 | | df-clab 2141 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵} ↔ [𝑤 / 𝑥]𝑧 ∈ 𝐵) |
13 | 10, 11, 12 | 3bitr4i 211 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)} ↔ 𝑤 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵}) |
14 | 13 | eqriv 2151 |
. . . . . 6
⊢ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)} = {𝑥 ∣ 𝑧 ∈ 𝐵} |
15 | 14 | eleq2i 2221 |
. . . . 5
⊢ (𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)} ↔ 𝐴 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵}) |
16 | | df-sbc 2934 |
. . . . . 6
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝐴 ∈ {𝑦 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}) |
17 | | df-sbc 2934 |
. . . . . . . . 9
⊢
([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵}) |
18 | | df-clab 2141 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵} ↔ [𝑦 / 𝑥]𝑧 ∈ 𝐵) |
19 | | sb6 1863 |
. . . . . . . . . 10
⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)) |
20 | 18, 19 | bitri 183 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵} ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)) |
21 | 17, 20 | bitri 183 |
. . . . . . . 8
⊢
([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)) |
22 | 21 | abbii 2270 |
. . . . . . 7
⊢ {𝑦 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)} |
23 | 22 | eleq2i 2221 |
. . . . . 6
⊢ (𝐴 ∈ {𝑦 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} ↔ 𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)}) |
24 | 16, 23 | bitri 183 |
. . . . 5
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝐵)}) |
25 | | df-sbc 2934 |
. . . . 5
⊢
([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝑧 ∈ 𝐵}) |
26 | 15, 24, 25 | 3bitr4i 211 |
. . . 4
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵) |
27 | 3, 26 | bitri 183 |
. . 3
⊢
([𝐴 / 𝑦]𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵) |
28 | 27 | abbii 2270 |
. 2
⊢ {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵} = {𝑧 ∣ [𝐴 / 𝑥]𝑧 ∈ 𝐵} |
29 | | df-csb 3028 |
. 2
⊢
⦋𝐴 /
𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐵} |
30 | | df-csb 3028 |
. 2
⊢
⦋𝐴 /
𝑥⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑥]𝑧 ∈ 𝐵} |
31 | 28, 29, 30 | 3eqtr4i 2185 |
1
⊢
⦋𝐴 /
𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 |