Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22Jun2011)
Ref  Expression  

Hypothesis  reseqi.1   A = B 

Assertion  reseq2i   ( C ` A ) = ( C ` B ) 
Step  Hyp  Ref  Expression 

1  reseqi.1   A = B 

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

3  1 2  axmp   ( C ` A ) = ( C ` B ) 