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

Metamath Proof Explorer

Theorem xpdisj2

Description: Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004)

		Ref	Expression
	Assertion	xpdisj2	$⊢ A \cap B = \emptyset \to (C \times A) \cap (D \times B) = \emptyset$

Step	Hyp	Ref	Expression
1		xpeq2	$⊢ A \cap B = \emptyset \to (C \cap D) \times (A \cap B) = (C \cap D) \times \emptyset$
2		inxp	$⊢ (C \times A) \cap (D \times B) = (C \cap D) \times (A \cap B)$
3		xp0	$⊢ (C \cap D) \times \emptyset = \emptyset$
4	3	eqcomi	$⊢ \emptyset = (C \cap D) \times \emptyset$
5	1 2 4	3eqtr4g	$⊢ A \cap B = \emptyset \to (C \times A) \cap (D \times B) = \emptyset$