Theorem disjresdisj

Description: The intersection of restrictions to disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		resindi	$$⊢{R\upharpoonright }_{\left(A\cap B\right)}=\left({R\upharpoonright }_A\right)\cap \left({R\upharpoonright }_B\right)$$
2		disjresin	$$⊢A\cap B=\varnothing \to {R\upharpoonright }_{\left(A\cap B\right)}=\varnothing$$
3	1 2	eqtr3id	$$⊢A\cap B=\varnothing \to \left({R\upharpoonright }_A\right)\cap \left({R\upharpoonright }_B\right)=\varnothing$$