Theorem xpindir

Description: Distributive law for Cartesian product over intersection. Similar to Theorem 102 of Suppes p. 52. (Contributed by NM, 26-Sep-2004)

	Ref	Expression
Assertion	xpindir	⊢ ( ( 𝐴 ∩ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		inxp	⊢ ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) × ( 𝐶 ∩ 𝐶 ) )
2		inidm	⊢ ( 𝐶 ∩ 𝐶 ) = 𝐶
3	2	xpeq2i	⊢ ( ( 𝐴 ∩ 𝐵 ) × ( 𝐶 ∩ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) × 𝐶 )
4	1 3	eqtr2i	⊢ ( ( 𝐴 ∩ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐶 ) )