Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993) Remove dependency on ax-10 . (Revised by BJ, 29-Nov-2020) (Proof shortened by SN, 20-Apr-2024) (Proof shortened by Wolf Lammen, 20-Jun-2025)