Theorem xpiundir

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

	Ref	Expression
Assertion	xpiundir	|- ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )

Proof

Step	Hyp	Ref	Expression
1		rexcom4	|- ( E. x e. A E. y ( y e. B /\ E. w e. C z = <. y , w >. ) <-> E. y E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
2		df-rex	|- ( E. y e. B E. w e. C z = <. y , w >. <-> E. y ( y e. B /\ E. w e. C z = <. y , w >. ) )
3	2	rexbii	|- ( E. x e. A E. y e. B E. w e. C z = <. y , w >. <-> E. x e. A E. y ( y e. B /\ E. w e. C z = <. y , w >. ) )
4		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
5	4	anbi1i	|- ( ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> ( E. x e. A y e. B /\ E. w e. C z = <. y , w >. ) )
6		r19.41v	|- ( E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) <-> ( E. x e. A y e. B /\ E. w e. C z = <. y , w >. ) )
7	5 6	bitr4i	|- ( ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
8	7	exbii	|- ( E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. y E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
9	1 3 8	3bitr4ri	|- ( E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. x e. A E. y e. B E. w e. C z = <. y , w >. )
10		df-rex	|- ( E. y e. U_ x e. A B E. w e. C z = <. y , w >. <-> E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) )
11		elxp2	|- ( z e. ( B X. C ) <-> E. y e. B E. w e. C z = <. y , w >. )
12	11	rexbii	|- ( E. x e. A z e. ( B X. C ) <-> E. x e. A E. y e. B E. w e. C z = <. y , w >. )
13	9 10 12	3bitr4i	|- ( E. y e. U_ x e. A B E. w e. C z = <. y , w >. <-> E. x e. A z e. ( B X. C ) )
14		elxp2	|- ( z e. ( U_ x e. A B X. C ) <-> E. y e. U_ x e. A B E. w e. C z = <. y , w >. )
15		eliun	|- ( z e. U_ x e. A ( B X. C ) <-> E. x e. A z e. ( B X. C ) )
16	13 14 15	3bitr4i	|- ( z e. ( U_ x e. A B X. C ) <-> z e. U_ x e. A ( B X. C ) )
17	16	eqriv	|- ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )