Description: Equality deduction for restrictions. (Contributed by NM, 21Oct2014)
Ref  Expression  

Hypothesis  reseqd.1   ( ph > A = B ) 

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

1  reseqd.1   ( ph > A = B ) 

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

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