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

Proof

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