Theorem xpdisj2

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

	Ref	Expression
Assertion	xpdisj2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 × 𝐴 ) ∩ ( 𝐷 × 𝐵 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		xpeq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 ∩ 𝐷 ) × ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐶 ∩ 𝐷 ) × ∅ ) )
2		inxp	⊢ ( ( 𝐶 × 𝐴 ) ∩ ( 𝐷 × 𝐵 ) ) = ( ( 𝐶 ∩ 𝐷 ) × ( 𝐴 ∩ 𝐵 ) )
3		xp0	⊢ ( ( 𝐶 ∩ 𝐷 ) × ∅ ) = ∅
4	3	eqcomi	⊢ ∅ = ( ( 𝐶 ∩ 𝐷 ) × ∅ )
5	1 2 4	3eqtr4g	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 × 𝐴 ) ∩ ( 𝐷 × 𝐵 ) ) = ∅ )