Syntax definition cab

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	class { 𝑥 ∣ 𝜑 }