Definition df-oprab 6319

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 6318 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 6459. (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 6316	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1454	. . . . . . . 8 class w
8	2	cv 1454	. . . . . . . . . 10 class x
9	3	cv 1454	. . . . . . . . . 10 class y
10	8, 9	cop 3986	. . . . . . . . 9 class <. x , y >.
11	4	cv 1454	. . . . . . . . 9 class z
12	10, 11	cop 3986	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1455	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 375	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1674	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1674	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1674	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2448	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1455	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6342  dfoprab2  6364  nfoprab1  6367  nfoprab2  6368  nfoprab3  6369  nfoprab  6370  oprabbid  6371  ssoprab2  6374  mpt20  6388  cbvoprab2  6391  eloprabga  6410  oprabrexex2  6810  eloprabi  6882  dftpos3  7017  meet0  16432  join0  16433  cnvoprab  28357  mppspstlem  30258  mppsval  30259  colinearex  30876  csboprabg  31776