Definition df-oprab

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 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 an operation given by a class abstraction is given by ovmpo . (Contributed by NM, 12-Mar-1995)

	Ref	Expression
Assertion	df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2		vz	$$setvarz$$
3		wph	$$wff\phi$$
4	3 0 1 2	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
5		vw	$$setvarw$$
6	5	cv	$$setvarw$$
7	0	cv	$$setvarx$$
8	1	cv	$$setvary$$
9	7 8	cop	$$class⟨x,y⟩$$
10	2	cv	$$setvarz$$
11	9 10	cop	$$class⟨⟨x,y⟩,z⟩$$
12	6 11	wceq	$$wffw=⟨⟨x,y⟩,z⟩$$
13	12 3	wa	$$wff\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
14	13 2	wex	$$wff\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
15	14 1	wex	$$wff\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
16	15 0	wex	$$wff\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
17	16 5	cab	$$class\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
18	4 17	wceq	$$wff\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$