Theorem xpsndisj

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

	Ref	Expression
Assertion	xpsndisj	$$⊢B\ne D\to \left(A\times \left\{B\right\}\right)\cap \left(C\times \left\{D\right\}\right)=\varnothing$$

Proof

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