Theorem resindm

Description: When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008)

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

Proof

Step	Hyp	Ref	Expression
1		resdm	$$⊢\mathrm{Rel}A\to {A\upharpoonright }_{\mathrm{dom}A}=A$$
2	1	ineq2d	$$⊢\mathrm{Rel}A\to \left({A\upharpoonright }_B\right)\cap \left({A\upharpoonright }_{\mathrm{dom}A}\right)=\left({A\upharpoonright }_B\right)\cap A$$
3		resindi	$$⊢{A\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}=\left({A\upharpoonright }_B\right)\cap \left({A\upharpoonright }_{\mathrm{dom}A}\right)$$
4		incom	$$⊢\left({A\upharpoonright }_B\right)\cap A=A\cap \left({A\upharpoonright }_B\right)$$
5		inres	$$⊢A\cap \left({A\upharpoonright }_B\right)={\left(A\cap A\right)\upharpoonright }_B$$
6		inidm	$$⊢A\cap A=A$$
7	6	reseq1i	$$⊢{\left(A\cap A\right)\upharpoonright }_B={A\upharpoonright }_B$$
8	4 5 7	3eqtrri	$$⊢{A\upharpoonright }_B=\left({A\upharpoonright }_B\right)\cap A$$
9	2 3 8	3eqtr4g	$$⊢\mathrm{Rel}A\to {A\upharpoonright }_{\left(B\cap \mathrm{dom}A\right)}={A\upharpoonright }_B$$