Description: Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | xpdisj1 | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐷 ) ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1 | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ 𝐵 ) × ( 𝐶 ∩ 𝐷 ) ) = ( ∅ × ( 𝐶 ∩ 𝐷 ) ) ) | |
2 | inxp | ⊢ ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐵 ) × ( 𝐶 ∩ 𝐷 ) ) | |
3 | 0xp | ⊢ ( ∅ × ( 𝐶 ∩ 𝐷 ) ) = ∅ | |
4 | 3 | eqcomi | ⊢ ∅ = ( ∅ × ( 𝐶 ∩ 𝐷 ) ) |
5 | 1 2 4 | 3eqtr4g | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐶 ) ∩ ( 𝐵 × 𝐷 ) ) = ∅ ) |