Theorem 3sstr3i

Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996) (Proof shortened by Eric Schmidt, 26-Jan-2007)

	Ref	Expression
Hypotheses	3sstr3.1	⊢ 𝐴 ⊆ 𝐵
	3sstr3.2	⊢ 𝐴 = 𝐶
	3sstr3.3	⊢ 𝐵 = 𝐷
Assertion	3sstr3i	⊢ 𝐶 ⊆ 𝐷

Proof

Step	Hyp	Ref	Expression
1		3sstr3.1	⊢ 𝐴 ⊆ 𝐵
2		3sstr3.2	⊢ 𝐴 = 𝐶
3		3sstr3.3	⊢ 𝐵 = 𝐷
4	2 3	sseq12i	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷 )
5	1 4	mpbi	⊢ 𝐶 ⊆ 𝐷