Description: Conversion of implicit substitution to explicit class substitution,
using a bound-variable hypothesis instead of distinct variables.
(Closed theorem version of sbciegf .) (Contributed by NM, 10-Nov-2005)(Revised by Mario Carneiro, 13-Oct-2016)(Proof
shortened by SN, 14-May-2025)