Syntax Definition crab 2447

Description: Extend class notation to include the restricted class abstraction (class builder).

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
crab	class {𝑥 ∈ 𝐴 ∣ 𝜑}

See definition df-rab 2452 for more information.