Step | Hyp | Ref
| Expression |
1 | | df-mpt 5111 |
. 2
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶)} |
2 | | df-mpo 7175 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷)} |
3 | | eliunxp2 45203 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
4 | 3 | anbi1i 627 |
. . . . . 6
⊢ ((𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶) ↔ (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶)) |
5 | | 19.41vv 1958 |
. . . . . 6
⊢
(∃𝑥∃𝑦((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶) ↔ (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶)) |
6 | | anass 472 |
. . . . . . . 8
⊢ (((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
7 | | mpomptx2.1 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) |
8 | 7 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑤 = 𝐶 ↔ 𝑤 = 𝐷)) |
9 | 8 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))) |
10 | 9 | pm5.32i 578 |
. . . . . . . 8
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))) |
11 | 6, 10 | bitri 278 |
. . . . . . 7
⊢ (((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))) |
12 | 11 | 2exbii 1855 |
. . . . . 6
⊢
(∃𝑥∃𝑦((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑤 = 𝐶) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))) |
13 | 4, 5, 12 | 3bitr2i 302 |
. . . . 5
⊢ ((𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))) |
14 | 13 | opabbii 5097 |
. . . 4
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶)} = {〈𝑧, 𝑤〉 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))} |
15 | | dfoprab2 7226 |
. . . 4
⊢
{〈〈𝑥,
𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷)} = {〈𝑧, 𝑤〉 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷))} |
16 | 14, 15 | eqtr4i 2764 |
. . 3
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶)} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐷)} |
17 | 2, 16 | eqtr4i 2764 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝑤 = 𝐶)} |
18 | 1, 17 | eqtr4i 2764 |
1
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |