This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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