Theorem iunin1

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use uniiun to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015)

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

Proof

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