Theorem resdmdfsn

Description: Restricting a class to its domain without a set is the same as restricting the class to the universe without this set. (Contributed by AV, 2-Dec-2018) Remove antecedent. (Revised by Eric Schmidt, 16-Jun-2026)

	Ref	Expression
Assertion	resdmdfsn	$$⊢{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	$$⊢{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		inv1	$$⊢\mathrm{dom}R\cap \mathrm{V}=\mathrm{dom}R$$
4	3	ineqcomi	$$⊢\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	2 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	1 7	eqtr3i	$$⊢{R\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={R\upharpoonright }_{\left(\mathrm{dom}R\setminus \left\{X\right\}\right)}$$