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	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		vz	|- z
3		wph	|- ph
4	3 0 1 2	coprab	|- { <. <. x , y >. , z >. | ph }
5		vw	|- w
6	5	cv	|- w
7	0	cv	|- x
8	1	cv	|- y
9	7 8	cop	|- <. x , y >.
10	2	cv	|- z
11	9 10	cop	|- <. <. x , y >. , z >.
12	6 11	wceq	|- w = <. <. x , y >. , z >.
13	12 3	wa	|- ( w = <. <. x , y >. , z >. /\ ph )
14	13 2	wex	|- E. z ( w = <. <. x , y >. , z >. /\ ph )
15	14 1	wex	|- E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
16	15 0	wex	|- E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph )
17	16 5	cab	|- { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
18	4 17	wceq	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }