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

Hypothesis  reseqd.1   ( ph > A = B ) 

Assertion  reseq2d   ( ph > ( C ` A ) = ( C ` B ) ) 
Step  Hyp  Ref  Expression 

1  reseqd.1   ( ph > A = B ) 

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

3  1 2  syl   ( ph > ( C ` A ) = ( C ` B ) ) 