Definition df-oprab 6200

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 6199 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 6337. (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 6197	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1398	. . . . . . . 8 class w
8	2	cv 1398	. . . . . . . . . 10 class x
9	3	cv 1398	. . . . . . . . . 10 class y
10	8, 9	cop 3950	. . . . . . . . 9 class <. x , y >.
11	4	cv 1398	. . . . . . . . 9 class z
12	10, 11	cop 3950	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1399	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 367	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1620	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1620	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1620	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2367	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1399	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6223  dfoprab2  6242  nfoprab1  6245  nfoprab2  6246  nfoprab3  6247  nfoprab  6248  oprabbid  6249  ssoprab2  6252  mpt20  6266  cbvoprab2  6269  eloprabga  6288  oprabrexex2  6689  eloprabi  6761  dftpos3  6891  meet0  15884  join0  15885  cnvoprab  27696  mppspstlem  29120  mppsval  29121  colinearex  29863