Description: Introduce the class abstraction (or class builder) notation:
{ x | ph } is the class of sets x such that ph ( x ) is true.
A setvar variable can be expressed as a class abstraction per theorem
cvjust , justifying the substitution of class variables for setvar
variables via the use of cv .