| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rexcom 3290 | . . . 4
⊢
(∃𝑤 ∈
𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑤 ∈ 𝐶 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉) | 
| 2 |  | eliun 4995 | . . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 3 | 2 | anbi1i 624 | . . . . . . 7
⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 4 | 3 | exbii 1848 | . . . . . 6
⊢
(∃𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 5 |  | df-rex 3071 | . . . . . 6
⊢
(∃𝑦 ∈
∪ 𝑥 ∈ 𝐴 𝐵𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑦(𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 6 |  | df-rex 3071 | . . . . . . . 8
⊢
(∃𝑦 ∈
𝐵 𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 7 | 6 | rexbii 3094 | . . . . . . 7
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 8 |  | rexcom4 3288 | . . . . . . 7
⊢
(∃𝑥 ∈
𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 9 |  | r19.41v 3189 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 10 | 9 | exbii 1848 | . . . . . . 7
⊢
(∃𝑦∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 11 | 7, 8, 10 | 3bitri 297 | . . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ 𝑧 = 〈𝑤, 𝑦〉)) | 
| 12 | 4, 5, 11 | 3bitr4i 303 | . . . . 5
⊢
(∃𝑦 ∈
∪ 𝑥 ∈ 𝐴 𝐵𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉) | 
| 13 | 12 | rexbii 3094 | . . . 4
⊢
(∃𝑤 ∈
𝐶 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑤 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉) | 
| 14 |  | elxp2 5709 | . . . . 5
⊢ (𝑧 ∈ (𝐶 × 𝐵) ↔ ∃𝑤 ∈ 𝐶 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉) | 
| 15 | 14 | rexbii 3094 | . . . 4
⊢
(∃𝑥 ∈
𝐴 𝑧 ∈ (𝐶 × 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑤 ∈ 𝐶 ∃𝑦 ∈ 𝐵 𝑧 = 〈𝑤, 𝑦〉) | 
| 16 | 1, 13, 15 | 3bitr4i 303 | . . 3
⊢
(∃𝑤 ∈
𝐶 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑧 = 〈𝑤, 𝑦〉 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ (𝐶 × 𝐵)) | 
| 17 |  | elxp2 5709 | . . 3
⊢ (𝑧 ∈ (𝐶 × ∪
𝑥 ∈ 𝐴 𝐵) ↔ ∃𝑤 ∈ 𝐶 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑧 = 〈𝑤, 𝑦〉) | 
| 18 |  | eliun 4995 | . . 3
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ (𝐶 × 𝐵)) | 
| 19 | 16, 17, 18 | 3bitr4i 303 | . 2
⊢ (𝑧 ∈ (𝐶 × ∪
𝑥 ∈ 𝐴 𝐵) ↔ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | 
| 20 | 19 | eqriv 2734 | 1
⊢ (𝐶 × ∪ 𝑥 ∈ 𝐴 𝐵) = ∪
𝑥 ∈ 𝐴 (𝐶 × 𝐵) |