Description: Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a that avoids the existential quantifiers of copsexg ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)