Description: An equivalence for class substitution. (Contributed by NM, 11-Oct-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)