# 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}×\bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in {A}}\left({C}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 rexcom ${⊢}\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
2 eliun ${⊢}{y}\in \bigcup _{{x}\in {A}}{B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
3 2 anbi1i ${⊢}\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {z}=⟨{w},{y}⟩\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
4 3 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {z}=⟨{w},{y}⟩\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
5 df-rex ${⊢}\exists {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \bigcup _{{x}\in {A}}{B}\wedge {z}=⟨{w},{y}⟩\right)$
6 df-rex ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
7 6 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
8 rexcom4 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
9 r19.41v ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
10 9 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
11 7 8 10 3bitri ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\wedge {z}=⟨{w},{y}⟩\right)$
12 4 5 11 3bitr4i ${⊢}\exists {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
13 12 rexbii ${⊢}\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
14 elxp2 ${⊢}{z}\in \left({C}×{B}\right)↔\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
15 14 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left({C}×{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
16 1 13 15 3bitr4i ${⊢}\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left({C}×{B}\right)$
17 elxp2 ${⊢}{z}\in \left({C}×\bigcup _{{x}\in {A}}{B}\right)↔\exists {w}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}=⟨{w},{y}⟩$
18 eliun ${⊢}{z}\in \bigcup _{{x}\in {A}}\left({C}×{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \left({C}×{B}\right)$
19 16 17 18 3bitr4i ${⊢}{z}\in \left({C}×\bigcup _{{x}\in {A}}{B}\right)↔{z}\in \bigcup _{{x}\in {A}}\left({C}×{B}\right)$
20 19 eqriv ${⊢}{C}×\bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in {A}}\left({C}×{B}\right)$