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