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		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\}$$
2		incom	$$⊢\mathrm{V}\cap \mathrm{dom}R=\mathrm{dom}R\cap \mathrm{V}$$
3		inv1	$$⊢\mathrm{dom}R\cap \mathrm{V}=\mathrm{dom}R$$
4	2 3	eqtri	$$⊢\mathrm{V}\cap \mathrm{dom}R=\mathrm{dom}R$$
5	4	difeq1i	$$⊢\left(\mathrm{V}\cap \mathrm{dom}R\right)\setminus \left\{X\right\}=\mathrm{dom}R\setminus \left\{X\right\}$$
6	1 5	eqtri	$$⊢\left(\mathrm{V}\setminus \left\{X\right\}\right)\cap \mathrm{dom}R=\mathrm{dom}R\setminus \left\{X\right\}$$
7	6	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)}$$
8		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)}$$
9	7 8	syl5reqr	$$⊢\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)}$$