Definition df-oprab 6654

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 6653 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 ovmpt2 6796. (Contributed by NM, 12-Mar-1995.)

Assertion

Ref	Expression
df-oprab	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

Distinct variable groups:   x, w   y, w   z, w   ph, w

Allowed substitution hints:   ph( x, y, z)

Detailed syntax breakdown of Definition df-oprab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		vz	. . 3 setvar z
5	1, 2, 3, 4	coprab 6651	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1482	. . . . . . . 8 class w
8	2	cv 1482	. . . . . . . . . 10 class x
9	3	cv 1482	. . . . . . . . . 10 class y
10	8, 9	cop 4183	. . . . . . . . 9 class <. x , y >.
11	4	cv 1482	. . . . . . . . 9 class z
12	10, 11	cop 4183	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1483	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 384	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1704	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1704	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1704	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2608	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1483	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6677  dfoprab2  6701  nfoprab1  6704  nfoprab2  6705  nfoprab3  6706  nfoprab  6707  oprabbid  6708  ssoprab2  6711  mpt20  6725  cbvoprab2  6728  eloprabga  6747  oprabrexex2  7158  eloprabi  7232  dftpos3  7370  meet0  17137  join0  17138  cnvoprab  29498  mppspstlem  31468  mppsval  31469  colinearex  32167  csboprabg  33176