Metamath Proof Explorer


Theorem eqimss2i

Description: Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007)

Ref Expression
Hypothesis eqimssi.1 A=B
Assertion eqimss2i BA

Proof

Step Hyp Ref Expression
1 eqimssi.1 A=B
2 ssid BB
3 2 1 sseqtrri BA