Metamath Proof Explorer


Theorem eqimssi

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

Ref Expression
Hypothesis eqimssi.1 A=B
Assertion eqimssi AB

Proof

Step Hyp Ref Expression
1 eqimssi.1 A=B
2 ssid AA
3 2 1 sseqtri AB