Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993) (Proof shortened by Andrew Salmon, 21-Jun-2011)