Metamath Proof Explorer


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 A B
3sstr3.2 A = C
3sstr3.3 B = D
Assertion 3sstr3i C D

Proof

Step Hyp Ref Expression
1 3sstr3.1 A B
2 3sstr3.2 A = C
3 3sstr3.3 B = D
4 2 3 sseq12i A B C D
5 1 4 mpbi C D