Theorem 2iunin

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

	Ref	Expression
Assertion	2iunin	$$⊢\bigcup _{x\in A}\bigcup _{y\in B}\left(C\cap D\right)=\bigcup _{x\in A}C\cap \bigcup _{y\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iunin2	$$⊢\bigcup _{y\in B}\left(C\cap D\right)=C\cap \bigcup _{y\in B}D$$
2	1	a1i	$$⊢x\in A\to \bigcup _{y\in B}\left(C\cap D\right)=C\cap \bigcup _{y\in B}D$$
3	2	iuneq2i	$$⊢\bigcup _{x\in A}\bigcup _{y\in B}\left(C\cap D\right)=\bigcup _{x\in A}\left(C\cap \bigcup _{y\in B}D\right)$$
4		iunin1	$$⊢\bigcup _{x\in A}\left(C\cap \bigcup _{y\in B}D\right)=\bigcup _{x\in A}C\cap \bigcup _{y\in B}D$$
5	3 4	eqtri	$$⊢\bigcup _{x\in A}\bigcup _{y\in B}\left(C\cap D\right)=\bigcup _{x\in A}C\cap \bigcup _{y\in B}D$$