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 .
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cab |