Syntax Definition copab2 3002

Description: Extend class notation to include class abstractions of nested ordered pairs.

Hypotheses

Ref	Expression
wph	wff ph
vx	set x
vy	set y
vz	set z

Assertion

Ref	Expression
copab2	class {<.<.x, y>., z>. | ph}

See definition df-oprab 3004 for more information.

metamath.org