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