Theorem bj-funidres

Description: The restricted identity relation is a function. (Contributed by BJ, 27-Dec-2023)

TODO: relabel funi to funid.

	Ref	Expression
Assertion	bj-funidres	$$⊢\mathrm{Fun}\left({\mathrm{I}\upharpoonright }_V\right)$$

Proof

Step	Hyp	Ref	Expression
1		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
2		funres	$$⊢\mathrm{Fun}\mathrm{I}\to \mathrm{Fun}\left({\mathrm{I}\upharpoonright }_V\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\left({\mathrm{I}\upharpoonright }_V\right)$$