Definition df-oprab 6285

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 6284 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 6423. (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 6282	. 2 class { <. <. x , y >. , z >. | ph }
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1382	. . . . . . . 8 class w
8	2	cv 1382	. . . . . . . . . 10 class x
9	3	cv 1382	. . . . . . . . . 10 class y
10	8, 9	cop 4020	. . . . . . . . 9 class <. x , y >.
11	4	cv 1382	. . . . . . . . 9 class z
12	10, 11	cop 4020	. . . . . . . 8 class <. <. x , y >. , z >.
13	7, 12	wceq 1383	. . . . . . 7 wff w = <. <. x , y >. , z >.
14	13, 1	wa 369	. . . . . 6 wff ( w = <. <. x , y >. , z >. /\ ph )
15	14, 4	wex 1599	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1599	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1599	. . 3 wff E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
18	17, 6	cab 2428	. 2 class { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
19	5, 18	wceq 1383	1 wff { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

This definition is referenced by:  oprabid  6308  dfoprab2  6328  nfoprab1  6331  nfoprab2  6332  nfoprab3  6333  nfoprab  6334  oprabbid  6335  ssoprab2  6338  mpt20  6352  cbvoprab2  6355  eloprabga  6374  oprabrexex2  6775  eloprabi  6847  dftpos3  6975  meet0  15746  join0  15747  cnvoprab  27524  mppspstlem  28909  mppsval  28910  colinearex  29686