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	$$⊢A\times \left(B\cap C\right)=\left(A\times B\right)\cap \left(A\times C\right)$$

Proof

Step	Hyp	Ref	Expression
1		inxp	$$⊢\left(A\times B\right)\cap \left(A\times C\right)=\left(A\cap A\right)\times \left(B\cap C\right)$$
2		inidm	$$⊢A\cap A=A$$
3	2	xpeq1i	$$⊢\left(A\cap A\right)\times \left(B\cap C\right)=A\times \left(B\cap C\right)$$
4	1 3	eqtr2i	$$⊢A\times \left(B\cap C\right)=\left(A\times B\right)\cap \left(A\times C\right)$$