Definition df-oprab 6309

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 6308 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 6446. (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 6306	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1436	. . . . . . . 8 class w
8	2	cv 1436	. . . . . . . . . 10 class x
9	3	cv 1436	. . . . . . . . . 10 class y
10	8, 9	cop 4008	. . . . . . . . 9 class <. x , y >.
11	4	cv 1436	. . . . . . . . 9 class z
12	10, 11	cop 4008	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1437	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 370	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1659	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1659	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1659	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2414	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1437	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6332  dfoprab2  6351  nfoprab1  6354  nfoprab2  6355  nfoprab3  6356  nfoprab  6357  oprabbid  6358  ssoprab2  6361  mpt20  6375  cbvoprab2  6378  eloprabga  6397  oprabrexex2  6797  eloprabi  6869  dftpos3  6999  meet0  16334  join0  16335  cnvoprab  28151  mppspstlem  29997  mppsval  29998  colinearex  30612