Theorem xpdisj2

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

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

Proof

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