Metamath Proof Explorer

Theorem xpiundi

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

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

Proof

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