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	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		iunin1	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 𝑥 ∩ 𝐵 )
2		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
3	2	ineq1i	⊢ ( ∪ 𝐴 ∩ 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 𝑥 ∩ 𝐵 )
4	1 3	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ( ∪ 𝐴 ∩ 𝐵 )