Definition df-oprab 6281

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 6280 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 6415. (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 6278	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1373	. . . . . . . 8 class w
8	2	cv 1373	. . . . . . . . . 10 class x
9	3	cv 1373	. . . . . . . . . 10 class y
10	8, 9	cop 4028	. . . . . . . . 9 class <. x , y >.
11	4	cv 1373	. . . . . . . . 9 class z
12	10, 11	cop 4028	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1374	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 369	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1591	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1591	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1591	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2447	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1374	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6301  dfoprab2  6320  nfoprab1  6323  nfoprab2  6324  nfoprab3  6325  nfoprab  6326  oprabbid  6327  ssoprab2  6330  mpt20  6344  cbvoprab2  6347  eloprabga  6366  oprabrexex2  6766  eloprabi  6838  dftpos3  6965  meet0  15615  join0  15616  cnvoprab  27206  colinearex  29275