Theorem resdmdfsn

Description: Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018)

	Ref	Expression
Assertion	resdmdfsn	$$⊢\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		resindm	$$⊢\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)}$$