This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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