Theorem xpdisj2

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

	Ref	Expression
Assertion	xpdisj2	|- ( ( A i^i B ) = (/) -> ( ( C X. A ) i^i ( D X. B ) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		xpeq2	|- ( ( A i^i B ) = (/) -> ( ( C i^i D ) X. ( A i^i B ) ) = ( ( C i^i D ) X. (/) ) )
2		inxp	|- ( ( C X. A ) i^i ( D X. B ) ) = ( ( C i^i D ) X. ( A i^i B ) )
3		xp0	|- ( ( C i^i D ) X. (/) ) = (/)
4	3	eqcomi	|- (/) = ( ( C i^i D ) X. (/) )
5	1 2 4	3eqtr4g	|- ( ( A i^i B ) = (/) -> ( ( C X. A ) i^i ( D X. B ) ) = (/) )