Theorem disjresdif

Description: The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024)

	Ref	Expression
Assertion	disjresdif	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)={R\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		disjresdisj	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_A\right)\cap \left({R\upharpoonright }_B\right)=\varnothing$$
2		disjdif2	$$⊢\left({R\upharpoonright }_A\right)\cap \left({R\upharpoonright }_B\right)=\varnothing \to \left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)={R\upharpoonright }_A$$
3	1 2	syl	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)={R\upharpoonright }_A$$