Step | Hyp | Ref
| Expression |
1 | | csbopab 5436 |
. . 3
⊢
⦋𝐴 /
𝑥⦌{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} |
2 | | sbcan 3746 |
. . . . 5
⊢
([𝐴 / 𝑥](𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝑌 ∧ [𝐴 / 𝑥]𝑧 = 𝑍)) |
3 | | sbcel12 4323 |
. . . . . . 7
⊢
([𝐴 / 𝑥]𝑦 ∈ 𝑌 ↔ ⦋𝐴 / 𝑥⦌𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌) |
4 | | csbconstg 3830 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦) |
5 | 4 | eleq1d 2822 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌)) |
6 | 3, 5 | syl5bb 286 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 ∈ 𝑌 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌)) |
7 | | sbceq2g 4331 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 = 𝑍 ↔ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍)) |
8 | 6, 7 | anbi12d 634 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑦 ∈ 𝑌 ∧ [𝐴 / 𝑥]𝑧 = 𝑍) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ∧ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍))) |
9 | 2, 8 | syl5bb 286 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ∧ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍))) |
10 | 9 | opabbidv 5119 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ∧ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍)}) |
11 | 1, 10 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ∧ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍)}) |
12 | | df-mpt 5136 |
. . 3
⊢ (𝑦 ∈ 𝑌 ↦ 𝑍) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} |
13 | 12 | csbeq2i 3819 |
. 2
⊢
⦋𝐴 /
𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍)} |
14 | | df-mpt 5136 |
. 2
⊢ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ∧ 𝑧 = ⦋𝐴 / 𝑥⦌𝑍)} |
15 | 11, 13, 14 | 3eqtr4g 2803 |
1
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) |