Theorem disjresin

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

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

Proof

Step	Hyp	Ref	Expression
1		reseq2	$$⊢A\cap B=\varnothing \to {R\upharpoonright }_{\left(A\cap B\right)}={R\upharpoonright }_{\varnothing }$$
2		res0	$$⊢{R\upharpoonright }_{\varnothing }=\varnothing$$
3	1 2	eqtrdi	$$⊢A\cap B=\varnothing \to {R\upharpoonright }_{\left(A\cap B\right)}=\varnothing$$