Description: Membership in a class abstraction, using implicit substitution and an intermediate setvar y to avoid ax-10 , ax-11 , ax-12 . It also avoids a disjoint variable condition on x and A . (Contributed by SN, 16-May-2024)