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 . This is
to elabg what sbievw2 is to sbievw . (Contributed by SN, 20-Apr-2024)