Theorem disjiminres

Description: Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021)

	Ref	Expression
Assertion	disjiminres	$$⊢DisjS\to Disj\left(R\cap \left({S\upharpoonright }_A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjimres	$$⊢DisjS\to Disj\left({S\upharpoonright }_A\right)$$
2		disjimin	$$⊢Disj\left({S\upharpoonright }_A\right)\to Disj\left(R\cap \left({S\upharpoonright }_A\right)\right)$$
3	1 2	syl	$$⊢DisjS\to Disj\left(R\cap \left({S\upharpoonright }_A\right)\right)$$