Theorem xpdisj1

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

	Ref	Expression
Assertion	xpdisj1	$$⊢A\cap B=\varnothing \to \left(A\times C\right)\cap \left(B\times D\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢A\cap B=\varnothing \to \left(A\cap B\right)\times \left(C\cap D\right)=\varnothing \times \left(C\cap D\right)$$
2		inxp	$$⊢\left(A\times C\right)\cap \left(B\times D\right)=\left(A\cap B\right)\times \left(C\cap D\right)$$
3		0xp	$$⊢\varnothing \times \left(C\cap D\right)=\varnothing$$
4	3	eqcomi	$$⊢\varnothing =\varnothing \times \left(C\cap D\right)$$
5	1 2 4	3eqtr4g	$$⊢A\cap B=\varnothing \to \left(A\times C\right)\cap \left(B\times D\right)=\varnothing$$