Description: Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | disjiminres | ⊢ ( Disj 𝑆 → Disj ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjimres | ⊢ ( Disj 𝑆 → Disj ( 𝑆 ↾ 𝐴 ) ) | |
2 | disjimin | ⊢ ( Disj ( 𝑆 ↾ 𝐴 ) → Disj ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) ) | |
3 | 1 2 | syl | ⊢ ( Disj 𝑆 → Disj ( 𝑅 ∩ ( 𝑆 ↾ 𝐴 ) ) ) |