| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | resopab 6051 | . . 3
⊢
({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} | 
| 2 |  | 19.42vv 1956 | . . . . 5
⊢
(∃𝑥∃𝑦(𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | 
| 3 |  | an12 645 | . . . . . . 7
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑))) | 
| 4 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ (𝐴 × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) | 
| 5 |  | opelxp 5720 | . . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | 
| 6 | 4, 5 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑤 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 7 | 6 | anbi1d 631 | . . . . . . . 8
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) | 
| 8 | 7 | pm5.32i 574 | . . . . . . 7
⊢ ((𝑤 = 〈𝑥, 𝑦〉 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) | 
| 9 | 3, 8 | bitri 275 | . . . . . 6
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) | 
| 10 | 9 | 2exbii 1848 | . . . . 5
⊢
(∃𝑥∃𝑦(𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) | 
| 11 | 2, 10 | bitr3i 277 | . . . 4
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))) | 
| 12 | 11 | opabbii 5209 | . . 3
⊢
{〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} | 
| 13 | 1, 12 | eqtri 2764 | . 2
⊢
({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} | 
| 14 |  | dfoprab2 7492 | . . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | 
| 15 | 14 | reseq1i 5992 | . 2
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = ({〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} ↾ (𝐴 × 𝐵)) | 
| 16 |  | dfoprab2 7492 | . 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))} | 
| 17 | 13, 15, 16 | 3eqtr4i 2774 | 1
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} |