Theorem fvresi

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

	Ref	Expression
Assertion	fvresi	⊢ ( 𝐵 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝐵 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝐵 ) = ( I ‘ 𝐵 ) )
2		fvi	⊢ ( 𝐵 ∈ 𝐴 → ( I ‘ 𝐵 ) = 𝐵 )
3	1 2	eqtrd	⊢ ( 𝐵 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝐵 ) = 𝐵 )