Step | Hyp | Ref
| Expression |
1 | | vex 3412 |
. . . . . 6
⊢ 𝑢 ∈ V |
2 | | vex 3412 |
. . . . . 6
⊢ 𝑣 ∈ V |
3 | 1, 2 | op1std 7771 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (1st ‘𝑧) = 𝑢) |
4 | 3 | csbeq1d 3815 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
5 | 1, 2 | op2ndd 7772 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (2nd ‘𝑧) = 𝑣) |
6 | 5 | csbeq1d 3815 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
7 | 6 | csbeq2dv 3818 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
8 | 4, 7 | eqtrd 2777 |
. . 3
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
9 | 8 | mpomptx 7323 |
. 2
⊢ (𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) = (𝑢 ∈ 𝐴, 𝑣 ∈ ⦋𝑢 / 𝑥⦌𝐵 ↦ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
10 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑢({𝑥} × 𝐵) |
11 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑥{𝑢} |
12 | | nfcsb1v 3836 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
13 | 11, 12 | nfxp 5584 |
. . . 4
⊢
Ⅎ𝑥({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
14 | | sneq 4551 |
. . . . 5
⊢ (𝑥 = 𝑢 → {𝑥} = {𝑢}) |
15 | | csbeq1a 3825 |
. . . . 5
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
16 | 14, 15 | xpeq12d 5582 |
. . . 4
⊢ (𝑥 = 𝑢 → ({𝑥} × 𝐵) = ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)) |
17 | 10, 13, 16 | cbviun 4945 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
18 | 17 | mpteq1i 5145 |
. 2
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) = (𝑧 ∈ ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
19 | | nfcv 2904 |
. . 3
⊢
Ⅎ𝑢𝐵 |
20 | | nfcv 2904 |
. . 3
⊢
Ⅎ𝑢𝐶 |
21 | | nfcv 2904 |
. . 3
⊢
Ⅎ𝑣𝐶 |
22 | | nfcsb1v 3836 |
. . 3
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
23 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑦𝑢 |
24 | | nfcsb1v 3836 |
. . . 4
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 |
25 | 23, 24 | nfcsbw 3838 |
. . 3
⊢
Ⅎ𝑦⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
26 | | csbeq1a 3825 |
. . . 4
⊢ (𝑦 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
27 | | csbeq1a 3825 |
. . . 4
⊢ (𝑥 = 𝑢 → ⦋𝑣 / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
28 | 26, 27 | sylan9eqr 2800 |
. . 3
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
29 | 19, 12, 20, 21, 22, 25, 15, 28 | cbvmpox 7304 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑢 ∈ 𝐴, 𝑣 ∈ ⦋𝑢 / 𝑥⦌𝐵 ↦ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
30 | 9, 18, 29 | 3eqtr4ri 2776 |
1
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |