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 xAB×C=xAB×C

Proof

Step Hyp Ref Expression
1 rexcom4 xAyyBwCz=ywyxAyBwCz=yw
2 df-rex yBwCz=ywyyBwCz=yw
3 2 rexbii xAyBwCz=ywxAyyBwCz=yw
4 eliun yxABxAyB
5 4 anbi1i yxABwCz=ywxAyBwCz=yw
6 r19.41v xAyBwCz=ywxAyBwCz=yw
7 5 6 bitr4i yxABwCz=ywxAyBwCz=yw
8 7 exbii yyxABwCz=ywyxAyBwCz=yw
9 1 3 8 3bitr4ri yyxABwCz=ywxAyBwCz=yw
10 df-rex yxABwCz=ywyyxABwCz=yw
11 elxp2 zB×CyBwCz=yw
12 11 rexbii xAzB×CxAyBwCz=yw
13 9 10 12 3bitr4i yxABwCz=ywxAzB×C
14 elxp2 zxAB×CyxABwCz=yw
15 eliun zxAB×CxAzB×C
16 13 14 15 3bitr4i zxAB×CzxAB×C
17 16 eqriv xAB×C=xAB×C