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)
|- ( x = y -> ( ph <-> ps ) )
|- ( y = A -> ( ps <-> ch ) )
|- B = { x | ph }
|- ( A e. V -> ( A e. B <-> ch ) )
|- ( A e. B <-> A e. { x | ph } )
|- ( A e. V -> ( A e. { x | ph } <-> ch ) )