Theorem disjresundif

Description: Lemma for ressucdifsn2 . (Contributed by Peter Mazsa, 24-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		resundi	$$⊢{R\upharpoonright }_{\left(A\cup B\right)}=\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)$$
2	1	difeq1i	$$⊢\left({R\upharpoonright }_{\left(A\cup B\right)}\right)\setminus \left({R\upharpoonright }_B\right)=\left(\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)\right)\setminus \left({R\upharpoonright }_B\right)$$
3		difun2	$$⊢\left(\left({R\upharpoonright }_A\right)\cup \left({R\upharpoonright }_B\right)\right)\setminus \left({R\upharpoonright }_B\right)=\left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)$$
4	2 3	eqtri	$$⊢\left({R\upharpoonright }_{\left(A\cup B\right)}\right)\setminus \left({R\upharpoonright }_B\right)=\left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)$$
5		disjresdif	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_A\right)\setminus \left({R\upharpoonright }_B\right)={R\upharpoonright }_A$$
6	4 5	eqtrid	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_{\left(A\cup B\right)}\right)\setminus \left({R\upharpoonright }_B\right)={R\upharpoonright }_A$$