| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . 6
⊢ 𝑢 ∈ V |
| 2 | | vex 3484 |
. . . . . 6
⊢ 𝑣 ∈ V |
| 3 | 1, 2 | op1std 8024 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (1st ‘𝑧) = 𝑢) |
| 4 | 3 | csbeq1d 3903 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
| 5 | 1, 2 | op2ndd 8025 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (2nd ‘𝑧) = 𝑣) |
| 6 | 5 | csbeq1d 3903 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
| 7 | 6 | csbeq2dv 3906 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 8 | 4, 7 | eqtrd 2777 |
. . 3
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 9 | 8 | mpomptx 7546 |
. 2
⊢ (𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) = (𝑢 ∈ 𝐴, 𝑣 ∈ ⦋𝑢 / 𝑥⦌𝐵 ↦ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 10 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑢({𝑥} × 𝐵) |
| 11 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥{𝑢} |
| 12 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
| 13 | 11, 12 | nfxp 5718 |
. . . 4
⊢
Ⅎ𝑥({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
| 14 | | sneq 4636 |
. . . . 5
⊢ (𝑥 = 𝑢 → {𝑥} = {𝑢}) |
| 15 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
| 16 | 14, 15 | xpeq12d 5716 |
. . . 4
⊢ (𝑥 = 𝑢 → ({𝑥} × 𝐵) = ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)) |
| 17 | 10, 13, 16 | cbviun 5036 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
| 18 | 17 | mpteq1i 5238 |
. 2
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) = (𝑧 ∈ ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
| 19 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑢𝐵 |
| 20 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑢𝐶 |
| 21 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑣𝐶 |
| 22 | | nfcsb1v 3923 |
. . 3
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
| 23 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦𝑢 |
| 24 | | nfcsb1v 3923 |
. . . 4
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 |
| 25 | 23, 24 | nfcsbw 3925 |
. . 3
⊢
Ⅎ𝑦⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
| 26 | | csbeq1a 3913 |
. . . 4
⊢ (𝑦 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
| 27 | | csbeq1a 3913 |
. . . 4
⊢ (𝑥 = 𝑢 → ⦋𝑣 / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 28 | 26, 27 | sylan9eqr 2799 |
. . 3
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 29 | 19, 12, 20, 21, 22, 25, 15, 28 | cbvmpox 7526 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑢 ∈ 𝐴, 𝑣 ∈ ⦋𝑢 / 𝑥⦌𝐵 ↦ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 30 | 9, 18, 29 | 3eqtr4ri 2776 |
1
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |