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	⊢ Fun ( I ↾ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		funi	⊢ Fun I
2		funres	⊢ ( Fun I → Fun ( I ↾ 𝑉 ) )
3	1 2	ax-mp	⊢ Fun ( I ↾ 𝑉 )