Metamath Proof Explorer


Theorem indir

Description: Distributive law for intersection over union. Theorem 28 of Suppes p. 27. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion indir ( ( 𝐴𝐵 ) ∩ 𝐶 ) = ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 indi ( 𝐶 ∩ ( 𝐴𝐵 ) ) = ( ( 𝐶𝐴 ) ∪ ( 𝐶𝐵 ) )
2 incom ( ( 𝐴𝐵 ) ∩ 𝐶 ) = ( 𝐶 ∩ ( 𝐴𝐵 ) )
3 incom ( 𝐴𝐶 ) = ( 𝐶𝐴 )
4 incom ( 𝐵𝐶 ) = ( 𝐶𝐵 )
5 3 4 uneq12i ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) ) = ( ( 𝐶𝐴 ) ∪ ( 𝐶𝐵 ) )
6 1 2 5 3eqtr4i ( ( 𝐴𝐵 ) ∩ 𝐶 ) = ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) )