Metamath Proof Explorer


Theorem eqimss2

Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003)

Ref Expression
Assertion eqimss2
|- ( B = A -> A C_ B )

Proof

Step Hyp Ref Expression
1 eqimss
 |-  ( A = B -> A C_ B )
2 1 eqcoms
 |-  ( B = A -> A C_ B )