Syntax Definition coprab 5923

Description: Extend class notation to include class abstraction (class builder) of nested ordered pairs.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
vy	setvar 𝑦
vz	setvar 𝑧

Assertion

Ref	Expression
coprab	class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

See definition df-oprab 5926 for more information.