Syntax Definition cab 2716

Description: Introduce the class abstraction (or class builder) notation: {𝑥 ∣ 𝜑} is the class of sets 𝑥 such that 𝜑(𝑥) is true. A setvar variable can be expressed as a class abstraction per Theorem cvjust 2733, justifying the substitution of class variables for setvar variables via the use of cv 1538.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥

Assertion

Ref	Expression
cab	class {𝑥 ∣ 𝜑}

See definition df-clab 2717 for more information.