Theorem uniin1

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	uniin1	$$⊢\bigcup _{x\in A}\left(x\cap B\right)=\bigcup A\cap B$$

Proof

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