Definition df-oprab 5529

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 5527 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 ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-oprab	|- {<.<.x, y>., z>. | ph} = {w | E.xE.yE.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 5528	. 2 class {<.<.x, y>., z>. | ph}
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1641	. . . . . . . 8 class w
8	2	cv 1641	. . . . . . . . . 10 class x
9	3	cv 1641	. . . . . . . . . 10 class y
10	8, 9	cop 4562	. . . . . . . . 9 class <.x, y>.
11	4	cv 1641	. . . . . . . . 9 class z
12	10, 11	cop 4562	. . . . . . . 8 class <.<.x, y>., z>.
13	7, 12	wceq 1642	. . . . . . 7 wff w = <.<.x, y>., z>.
14	13, 1	wa 358	. . . . . 6 wff (w = <.<.x, y>., z>. /\ ph)
15	14, 4	wex 1541	. . . . 5 wff E.z(w = <.<.x, y>., z>. /\ ph)
16	15, 3	wex 1541	. . . 4 wff E.yE.z(w = <.<.x, y>., z>. /\ ph)
17	16, 2	wex 1541	. . 3 wff E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)
18	17, 6	cab 2339	. 2 class {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}
19	5, 18	wceq 1642	1 wff {<.<.x, y>., z>. | ph} = {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}

This definition is referenced by:  nfoprab1  5547  nfoprab2  5548  nfoprab3  5549  nfoprab  5550  oprabid  5551  dfoprab2  5559  hboprab1  5560  hboprab2  5561  hboprab3  5562  hboprab  5563  oprabbid  5564  cbvoprab2  5569  eloprabga  5579