Syntax definition cab

Description: Introduce the class builder or class abstraction notation ("the class of sets x such that ph "). Our class variables A , B , etc. range over class builders (implicitly in the case of defined class terms such as df-nul ). Note that a setvar variable can be expressed as a class builder per theorem cvjust , justifying the assignment of setvar variables to class variables via the use of cv .

	Ref	Expression
Assertion	cab	class { 𝑥 ∣ 𝜑 }