Step | Hyp | Ref
| Expression |
1 | | nfv 1913 |
. . . . 5
⊢
Ⅎ𝑧 𝑥 ∈ 𝐴 |
2 | | cbvmpox.1 |
. . . . . 6
⊢
Ⅎ𝑧𝐵 |
3 | 2 | nfcri 2889 |
. . . . 5
⊢
Ⅎ𝑧 𝑦 ∈ 𝐵 |
4 | 1, 3 | nfan 1898 |
. . . 4
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
5 | | cbvmpox.3 |
. . . . 5
⊢
Ⅎ𝑧𝐶 |
6 | 5 | nfeq2 2919 |
. . . 4
⊢
Ⅎ𝑧 𝑢 = 𝐶 |
7 | 4, 6 | nfan 1898 |
. . 3
⊢
Ⅎ𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = 𝐶) |
8 | | nfv 1913 |
. . . . 5
⊢
Ⅎ𝑤 𝑥 ∈ 𝐴 |
9 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑤𝐵 |
10 | 9 | nfcri 2889 |
. . . . 5
⊢
Ⅎ𝑤 𝑦 ∈ 𝐵 |
11 | 8, 10 | nfan 1898 |
. . . 4
⊢
Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | | cbvmpox.4 |
. . . . 5
⊢
Ⅎ𝑤𝐶 |
13 | 12 | nfeq2 2919 |
. . . 4
⊢
Ⅎ𝑤 𝑢 = 𝐶 |
14 | 11, 13 | nfan 1898 |
. . 3
⊢
Ⅎ𝑤((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = 𝐶) |
15 | | nfv 1913 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
16 | | cbvmpox.2 |
. . . . . 6
⊢
Ⅎ𝑥𝐷 |
17 | 16 | nfcri 2889 |
. . . . 5
⊢
Ⅎ𝑥 𝑤 ∈ 𝐷 |
18 | 15, 17 | nfan 1898 |
. . . 4
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) |
19 | | cbvmpox.5 |
. . . . 5
⊢
Ⅎ𝑥𝐸 |
20 | 19 | nfeq2 2919 |
. . . 4
⊢
Ⅎ𝑥 𝑢 = 𝐸 |
21 | 18, 20 | nfan 1898 |
. . 3
⊢
Ⅎ𝑥((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 = 𝐸) |
22 | | nfv 1913 |
. . . 4
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) |
23 | | cbvmpox.6 |
. . . . 5
⊢
Ⅎ𝑦𝐸 |
24 | 23 | nfeq2 2919 |
. . . 4
⊢
Ⅎ𝑦 𝑢 = 𝐸 |
25 | 22, 24 | nfan 1898 |
. . 3
⊢
Ⅎ𝑦((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 = 𝐸) |
26 | | eleq1w 2816 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
27 | 26 | adantr 480 |
. . . . 5
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
28 | | cbvmpox.7 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷) |
29 | 28 | eleq2d 2819 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐷)) |
30 | | eleq1w 2816 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐷 ↔ 𝑤 ∈ 𝐷)) |
31 | 29, 30 | sylan9bb 509 |
. . . . 5
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐷)) |
32 | 27, 31 | anbi12d 630 |
. . . 4
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷))) |
33 | | cbvmpox.8 |
. . . . 5
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸) |
34 | 33 | eqeq2d 2744 |
. . . 4
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑢 = 𝐶 ↔ 𝑢 = 𝐸)) |
35 | 32, 34 | anbi12d 630 |
. . 3
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 = 𝐸))) |
36 | 7, 14, 21, 25, 35 | cbvoprab12 7384 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑢〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = 𝐶)} = {〈〈𝑧, 𝑤〉, 𝑢〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 = 𝐸)} |
37 | | df-mpo 7300 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑢〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = 𝐶)} |
38 | | df-mpo 7300 |
. 2
⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸) = {〈〈𝑧, 𝑤〉, 𝑢〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷) ∧ 𝑢 = 𝐸)} |
39 | 36, 37, 38 | 3eqtr4i 2771 |
1
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸) |