Theorem eqsstrri

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

	Ref	Expression
Hypotheses	eqsstr3.1	⊢ 𝐵 = 𝐴
	eqsstr3.2	⊢ 𝐵 ⊆ 𝐶
Assertion	eqsstrri	⊢ 𝐴 ⊆ 𝐶

Proof

Step	Hyp	Ref	Expression
1		eqsstr3.1	⊢ 𝐵 = 𝐴
2		eqsstr3.2	⊢ 𝐵 ⊆ 𝐶
3	1	eqcomi	⊢ 𝐴 = 𝐵
4	3 2	eqsstri	⊢ 𝐴 ⊆ 𝐶