Theorem resindmOLD

Description: Obsolete version of resindm as of 16-Jun-2026. (Contributed by FL, 6-Oct-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	resindmOLD	$$⊢\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$$