Theorem xpdisj1

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

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

Proof

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