Syntax Definition cab 1090

Description: Introduce class abstraction notation ('the class of sets x such that φ is true'). Some classes defined with this notation are not sets, i.e. do not exist.

Hypotheses

Ref	Expression
wph	wff φ
vx	set x

Assertion

Ref	Expression
cab	class {x∣φ}

See definition df-clab 1093 for more information.

metamath.org