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

Metamath Proof Explorer

Theorem xpsndisj

Description: Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004)

		Ref	Expression
	Assertion	xpsndisj	$⊢ B \neq D \to (A \times \{B\}) \cap (C \times \{D\}) = \emptyset$

Step	Hyp	Ref	Expression
1		disjsn2	$⊢ B \neq D \to \{B\} \cap \{D\} = \emptyset$
2		xpdisj2	$⊢ \{B\} \cap \{D\} = \emptyset \to (A \times \{B\}) \cap (C \times \{D\}) = \emptyset$
3	1 2	syl	$⊢ B \neq D \to (A \times \{B\}) \cap (C \times \{D\}) = \emptyset$