Definition df-oprab 6253

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 6252 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 6390. (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 6250	. 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 3947	. . . . . . . . 9 class <. x , y >.
11	4	cv 1436	. . . . . . . . 9 class z
12	10, 11	cop 3947	. . . . . . . 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 1657	. . . . 5 wff E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15, 3	wex 1657	. . . 4 wff E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16, 2	wex 1657	. . 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  6276  dfoprab2  6295  nfoprab1  6298  nfoprab2  6299  nfoprab3  6300  nfoprab  6301  oprabbid  6302  ssoprab2  6305  mpt20  6319  cbvoprab2  6322  eloprabga  6341  oprabrexex2  6741  eloprabi  6813  dftpos3  6946  meet0  16326  join0  16327  cnvoprab  28258  mppspstlem  30161  mppsval  30162  colinearex  30776  csboprabg  31638