Syntax Definition cab 2714

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 2731, justifying the substitution of class variables for setvar variables via the use of cv 1539.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥

Assertion

Ref	Expression
cab	class {𝑥 ∣ 𝜑}

See definition df-clab 2715 for more information.