Syntax Definition cab 2715

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 2732, 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 2716 for more information.