Theorem fvresi

Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004)

	Ref	Expression
Assertion	fvresi	$$⊢B\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(B\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		fvres	$$⊢B\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(B\right)=\mathrm{I}\left(B\right)$$
2		fvi	$$⊢B\in A\to \mathrm{I}\left(B\right)=B$$
3	1 2	eqtrd	$$⊢B\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(B\right)=B$$