Description: The membership relation and the membership predicate agree when the
"containing" class is a setvar. Definition 1.6 of Schloeder p. 1.
(Contributed by NM, 13-Aug-1995) Replace the first setvar variable with
a class variable. (Revised by BJ, 13-Sep-2022)