Theorem 2iunin

Description: Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008)

	Ref	Expression
Assertion	2iunin	|- U_ x e. A U_ y e. B ( C i^i D ) = ( U_ x e. A C i^i U_ y e. B D )

Proof

Step	Hyp	Ref	Expression
1		iunin2	|- U_ y e. B ( C i^i D ) = ( C i^i U_ y e. B D )
2	1	a1i	|- ( x e. A -> U_ y e. B ( C i^i D ) = ( C i^i U_ y e. B D ) )
3	2	iuneq2i	|- U_ x e. A U_ y e. B ( C i^i D ) = U_ x e. A ( C i^i U_ y e. B D )
4		iunin1	|- U_ x e. A ( C i^i U_ y e. B D ) = ( U_ x e. A C i^i U_ y e. B D )
5	3 4	eqtri	|- U_ x e. A U_ y e. B ( C i^i D ) = ( U_ x e. A C i^i U_ y e. B D )