Metamath Proof Explorer
Description: Equality implies the subclass relation. (Contributed by NM, 21Jun1993)
(Proof shortened by Andrew Salmon, 21Jun2011)


Ref 
Expression 

Assertion 
eqimss 
$${\u22a2}{A}={B}\to {A}\subseteq {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqss 
$${\u22a2}{A}={B}\leftrightarrow \left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$$ 
2 
1

simplbi 
$${\u22a2}{A}={B}\to {A}\subseteq {B}$$ 