Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | eqimss2 | |- ( B = A -> A C_ B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss | |- ( A = B -> A C_ B ) |
|
2 | 1 | eqcoms | |- ( B = A -> A C_ B ) |