Step | Hyp | Ref
| Expression |
1 | | resopab 4933 |
. . 3
⊢
({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} |
2 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
3 | | an12 556 |
. . . . . . 7
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑))) |
4 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ (𝐴 × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
5 | | opelxp 4639 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
6 | 4, 5 | bitrdi 195 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
7 | 6 | anbi1d 462 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) |
8 | 7 | pm5.32i 451 |
. . . . . . 7
⊢ ((𝑤 = 〈𝑥, 𝑦〉 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) |
9 | 3, 8 | bitri 183 |
. . . . . 6
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) |
10 | 9 | 2exbii 1599 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) |
11 | 2, 10 | bitr3i 185 |
. . . 4
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) |
12 | 11 | opabbii 4054 |
. . 3
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} |
13 | 1, 12 | eqtri 2191 |
. 2
⊢
({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} |
14 | | dfoprab2 5897 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 14 | reseq1i 4885 |
. 2
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = ({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) |
16 | | dfoprab2 5897 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} |
17 | 13, 15, 16 | 3eqtr4i 2201 |
1
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} |