Theorem resiexd

Description: The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020)

	Ref	Expression
Hypothesis	resiexd.b	$$⊢\phi \to B\in V$$
Assertion	resiexd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		resiexd.b	$$⊢\phi \to B\in V$$
2		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
3		resfunexg	$$⊢\left(\mathrm{Fun}\mathrm{I}\wedge B\in V\right)\to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
4	2 1 3	sylancr	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$