Theorem resiima

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

	Ref	Expression
Assertion	resiima	|- ( B C_ A -> ( ( _I |` A ) " B ) = B )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( ( _I |` A ) " B ) = ran ( ( _I |` A ) |` B )
2	1	a1i	|- ( B C_ A -> ( ( _I |` A ) " B ) = ran ( ( _I |` A ) |` B ) )
3		resabs1	|- ( B C_ A -> ( ( _I |` A ) |` B ) = ( _I |` B ) )
4	3	rneqd	|- ( B C_ A -> ran ( ( _I |` A ) |` B ) = ran ( _I |` B ) )
5		rnresi	|- ran ( _I |` B ) = B
6	5	a1i	|- ( B C_ A -> ran ( _I |` B ) = B )
7	2 4 6	3eqtrd	|- ( B C_ A -> ( ( _I |` A ) " B ) = B )