Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4Apr1995)
Ref  Expression  

Hypotheses  sseqtrri.1   A C_ B 

sseqtrri.2   C = B 

Assertion  sseqtrri   A C_ C 
Step  Hyp  Ref  Expression 

1  sseqtrri.1   A C_ B 

2  sseqtrri.2   C = B 

3  2  eqcomi   B = C 
4  1 3  sseqtri   A C_ C 