Syntax Definition cab 1090

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

Hypotheses

Ref	Expression
wph	wff ph
vx	set x

Assertion

Ref	Expression
cab	class {x | ph}

See definition df-clab 1093 for more information.

metamath.org