Theorem eqsstrri

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999)

	Ref	Expression
Hypotheses	eqsstr3.1	|- B = A
	eqsstr3.2	|- B C_ C
Assertion	eqsstrri	|- A C_ C

Proof

Step	Hyp	Ref	Expression
1		eqsstr3.1	|- B = A
2		eqsstr3.2	|- B C_ C
3	1	eqcomi	|- A = B
4	3 2	eqsstri	|- A C_ C