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×xAB=xAC×B

Proof

Step Hyp Ref Expression
1 rexcom wCxAyBz=wyxAwCyBz=wy
2 eliun yxABxAyB
3 2 anbi1i yxABz=wyxAyBz=wy
4 3 exbii yyxABz=wyyxAyBz=wy
5 df-rex yxABz=wyyyxABz=wy
6 df-rex yBz=wyyyBz=wy
7 6 rexbii xAyBz=wyxAyyBz=wy
8 rexcom4 xAyyBz=wyyxAyBz=wy
9 r19.41v xAyBz=wyxAyBz=wy
10 9 exbii yxAyBz=wyyxAyBz=wy
11 7 8 10 3bitri xAyBz=wyyxAyBz=wy
12 4 5 11 3bitr4i yxABz=wyxAyBz=wy
13 12 rexbii wCyxABz=wywCxAyBz=wy
14 elxp2 zC×BwCyBz=wy
15 14 rexbii xAzC×BxAwCyBz=wy
16 1 13 15 3bitr4i wCyxABz=wyxAzC×B
17 elxp2 zC×xABwCyxABz=wy
18 eliun zxAC×BxAzC×B
19 16 17 18 3bitr4i zC×xABzxAC×B
20 19 eqriv C×xAB=xAC×B