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

Proof

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