Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of Quine p. 44. (Contributed by NM, 14-Apr-1995) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)