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

Proof

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