Theorem xpsndisj

Description: Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004)

	Ref	Expression
Assertion	xpsndisj	⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 × { 𝐵 } ) ∩ ( 𝐶 × { 𝐷 } ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		disjsn2	⊢ ( 𝐵 ≠ 𝐷 → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
2		xpdisj2	⊢ ( ( { 𝐵 } ∩ { 𝐷 } ) = ∅ → ( ( 𝐴 × { 𝐵 } ) ∩ ( 𝐶 × { 𝐷 } ) ) = ∅ )
3	1 2	syl	⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 × { 𝐵 } ) ∩ ( 𝐶 × { 𝐷 } ) ) = ∅ )