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 B A

Proof

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