Metamath Proof Explorer

Theorem xpiundir

Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014)

Ref Expression
Assertion xpiundir ⊢ ⋃ x ∈ A B × C = ⋃ x ∈ A B × C

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ x ∈ A ∃ y y ∈ B ∧ ∃ w ∈ C z = y w ↔ ∃ y ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w
2 df-rex ⊢ ∃ y ∈ B ∃ w ∈ C z = y w ↔ ∃ y y ∈ B ∧ ∃ w ∈ C z = y w
3 2 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B ∃ w ∈ C z = y w ↔ ∃ x ∈ A ∃ y y ∈ B ∧ ∃ w ∈ C z = y w
4 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
5 4 anbi1i ⊢ y ∈ ⋃ x ∈ A B ∧ ∃ w ∈ C z = y w ↔ ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w
6 r19.41v ⊢ ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w ↔ ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w
7 5 6 bitr4i ⊢ y ∈ ⋃ x ∈ A B ∧ ∃ w ∈ C z = y w ↔ ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w
8 7 exbii ⊢ ∃ y y ∈ ⋃ x ∈ A B ∧ ∃ w ∈ C z = y w ↔ ∃ y ∃ x ∈ A y ∈ B ∧ ∃ w ∈ C z = y w
9 1 3 8 3bitr4ri ⊢ ∃ y y ∈ ⋃ x ∈ A B ∧ ∃ w ∈ C z = y w ↔ ∃ x ∈ A ∃ y ∈ B ∃ w ∈ C z = y w
10 df-rex ⊢ ∃ y ∈ ⋃ x ∈ A B ∃ w ∈ C z = y w ↔ ∃ y y ∈ ⋃ x ∈ A B ∧ ∃ w ∈ C z = y w
11 elxp2 ⊢ z ∈ B × C ↔ ∃ y ∈ B ∃ w ∈ C z = y w
12 11 rexbii ⊢ ∃ x ∈ A z ∈ B × C ↔ ∃ x ∈ A ∃ y ∈ B ∃ w ∈ C z = y w
13 9 10 12 3bitr4i ⊢ ∃ y ∈ ⋃ x ∈ A B ∃ w ∈ C z = y w ↔ ∃ x ∈ A z ∈ B × C
14 elxp2 ⊢ z ∈ ⋃ x ∈ A B × C ↔ ∃ y ∈ ⋃ x ∈ A B ∃ w ∈ C z = y w
15 eliun ⊢ z ∈ ⋃ x ∈ A B × C ↔ ∃ x ∈ A z ∈ B × C
16 13 14 15 3bitr4i ⊢ z ∈ ⋃ x ∈ A B × C ↔ z ∈ ⋃ x ∈ A B × C
17 16 eqriv ⊢ ⋃ x ∈ A B × C = ⋃ x ∈ A B × C