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