Description: Equality theorem for image. (Contributed by NM, 14Aug1994)
Ref  Expression  

Assertion  imaeq2   ( A = B > ( C " A ) = ( C " B ) ) 
Step  Hyp  Ref  Expression 

1  reseq2   ( A = B > ( C ` A ) = ( C ` B ) ) 

2  1  rneqd   ( A = B > ran ( C ` A ) = ran ( C ` B ) ) 
3  dfima   ( C " A ) = ran ( C ` A ) 

4  dfima   ( C " B ) = ran ( C ` B ) 

5  2 3 4  3eqtr4g   ( A = B > ( C " A ) = ( C " B ) ) 