Theorem resiima

Description: The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006)

	Ref	Expression
Assertion	resiima	⊢ ( 𝐵 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( ( I ↾ 𝐴 ) “ 𝐵 ) = ran ( ( I ↾ 𝐴 ) ↾ 𝐵 )
2	1	a1i	⊢ ( 𝐵 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝐵 ) = ran ( ( I ↾ 𝐴 ) ↾ 𝐵 ) )
3		resabs1	⊢ ( 𝐵 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) ↾ 𝐵 ) = ( I ↾ 𝐵 ) )
4	3	rneqd	⊢ ( 𝐵 ⊆ 𝐴 → ran ( ( I ↾ 𝐴 ) ↾ 𝐵 ) = ran ( I ↾ 𝐵 ) )
5		rnresi	⊢ ran ( I ↾ 𝐵 ) = 𝐵
6	5	a1i	⊢ ( 𝐵 ⊆ 𝐴 → ran ( I ↾ 𝐵 ) = 𝐵 )
7	2 4 6	3eqtrd	⊢ ( 𝐵 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝐵 ) = 𝐵 )