Theorem resdmdfsnOLD

Description: Obsolete version of resdmdfsn as of 16-Jun-2026. (Contributed by AV, 2-Dec-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	resdmdfsnOLD	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={R\upharpoonright }_{\left(\mathrm{dom}R\setminus \left\{X\right\}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		resindmOLD	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\left(\left(\mathrm{V}\setminus \left\{X\right\}\right)\cap \mathrm{dom}R\right)}={R\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}$$
2		indif1	$$⊢\left(\mathrm{V}\setminus \left\{X\right\}\right)\cap \mathrm{dom}R=\left(\mathrm{V}\cap \mathrm{dom}R\right)\setminus \left\{X\right\}$$
3		incom	$$⊢\mathrm{V}\cap \mathrm{dom}R=\mathrm{dom}R\cap \mathrm{V}$$
4		inv1	$$⊢\mathrm{dom}R\cap \mathrm{V}=\mathrm{dom}R$$
5	3 4	eqtri	$$⊢\mathrm{V}\cap \mathrm{dom}R=\mathrm{dom}R$$
6	5	difeq1i	$$⊢\left(\mathrm{V}\cap \mathrm{dom}R\right)\setminus \left\{X\right\}=\mathrm{dom}R\setminus \left\{X\right\}$$
7	2 6	eqtri	$$⊢\left(\mathrm{V}\setminus \left\{X\right\}\right)\cap \mathrm{dom}R=\mathrm{dom}R\setminus \left\{X\right\}$$
8	7	reseq2i	$$⊢{R\upharpoonright }_{\left(\left(\mathrm{V}\setminus \left\{X\right\}\right)\cap \mathrm{dom}R\right)}={R\upharpoonright }_{\left(\mathrm{dom}R\setminus \left\{X\right\}\right)}$$
9	1 8	eqtr3di	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={R\upharpoonright }_{\left(\mathrm{dom}R\setminus \left\{X\right\}\right)}$$