Syntax Definition copab 2055

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

Hypotheses

Ref	Expression
wph	wff φ
vx	set x
vy	set y

Assertion

Ref	Expression
copab	class {⟨x, y⟩∣φ}

See definition df-opab 2098 for more information.

metamath.org