Theorem xpindi

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

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

Proof

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