Metamath Proof Explorer


Definition df-oprab

Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of TakeutiZaring p. 14. Normally x , y , and z are distinct, although the definition doesn't strictly require it. See df-ov for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpo . (Contributed by NM, 12-Mar-1995)

Ref Expression
Assertion df-oprab x y z | φ = w | x y z w = x y z φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 vy setvar y
2 vz setvar z
3 wph wff φ
4 3 0 1 2 coprab class x y z | φ
5 vw setvar w
6 5 cv setvar w
7 0 cv setvar x
8 1 cv setvar y
9 7 8 cop class x y
10 2 cv setvar z
11 9 10 cop class x y z
12 6 11 wceq wff w = x y z
13 12 3 wa wff w = x y z φ
14 13 2 wex wff z w = x y z φ
15 14 1 wex wff y z w = x y z φ
16 15 0 wex wff x y z w = x y z φ
17 16 5 cab class w | x y z w = x y z φ
18 4 17 wceq wff x y z | φ = w | x y z w = x y z φ