Description: Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | xpdisjres | ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res | ⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) | |
2 | xpdisj1 | ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) = ∅ ) | |
3 | 1 2 | syl5eq | ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ∅ ) |