Theorem eqsstri

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995)

	Ref	Expression
Hypotheses	eqsstr.1	|- A = B
	eqsstr.2	|- B C_ C
Assertion	eqsstri	|- A C_ C

Proof

Step	Hyp	Ref	Expression
1		eqsstr.1	|- A = B
2		eqsstr.2	|- B C_ C
3	1	sseq1i	|- ( A C_ C <-> B C_ C )
4	2 3	mpbir	|- A C_ C