Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)