Metamath Proof Explorer
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4Apr1995)


Ref 
Expression 

Hypotheses 
sseqtrri.1 
$${\u22a2}{A}\subseteq {B}$$ 


sseqtrri.2 
$${\u22a2}{C}={B}$$ 

Assertion 
sseqtrri 
$${\u22a2}{A}\subseteq {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sseqtrri.1 
$${\u22a2}{A}\subseteq {B}$$ 
2 

sseqtrri.2 
$${\u22a2}{C}={B}$$ 
3 
2

eqcomi 
$${\u22a2}{B}={C}$$ 
4 
1 3

sseqtri 
$${\u22a2}{A}\subseteq {C}$$ 