Theorem resindm

Description: When restricting a class, intersecting with the domain of the class has no effect. (Contributed by FL, 6-Oct-2008) Remove antecedent. (Revised by Eric Schmidt, 16-Jun-2026)

	Ref	Expression
Assertion	resindm	$$⊢{A\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=B\cap \mathrm{dom}A$$
2	1	reseq2i	$$⊢{\left({A\upharpoonright }_B\right)\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={\left({A\upharpoonright }_B\right)\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}$$
3		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$
4		resdm	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)\to {\left({A\upharpoonright }_B\right)\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={A\upharpoonright }_B$$
5	3 4	ax-mp	$$⊢{\left({A\upharpoonright }_B\right)\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={A\upharpoonright }_B$$
6		inss1	$$⊢B\cap \mathrm{dom}A\subseteq B$$
7	6	resabs1i	$$⊢{\left({A\upharpoonright }_B\right)\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}={A\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}$$
8	2 5 7	3eqtr3ri	$$⊢{A\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}={A\upharpoonright }_B$$