HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition copab2 3964
Description: Extend class notation to include class abstraction (class builder) 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 3966 for more information.
Colors of variables: wff set class
Copyright terms: Public domain