Theorem uniin2

Description: Union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		iunin2	$$⊢\bigcup _{x\in B}\left(A\cap x\right)=A\cap \bigcup _{x\in B}x$$
2		uniiun	$$⊢\bigcup B=\bigcup _{x\in B}x$$
3	2	ineq2i	$$⊢A\cap \bigcup B=A\cap \bigcup _{x\in B}x$$
4	1 3	eqtr4i	$$⊢\bigcup _{x\in B}\left(A\cap x\right)=A\cap \bigcup B$$