Metamath Proof Explorer


Theorem eqimss2

Description: Equality implies inclusion. (Contributed by NM, 23-Nov-2003)

Ref Expression
Assertion eqimss2 ⊢ B = A → A ⊆ B

Proof

Step Hyp Ref Expression
1 eqimss ⊢ A = B → A ⊆ B
2 1 eqcoms ⊢ B = A → A ⊆ B