Definition df-opab 4044

Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

Distinct variable groups:   x, z   y, z   ph, z

Allowed substitution hints:   ph( x, y)

Detailed syntax breakdown of Definition df-opab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4	1, 2, 3	copab 4042	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1342	. . . . . . 7 class z
7	2	cv 1342	. . . . . . . 8 class x
8	3	cv 1342	. . . . . . . 8 class y
9	7, 8	cop 3579	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1343	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 103	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1480	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1480	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2151	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1343	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4046  opabbid  4047  nfopab  4050  nfopab1  4051  nfopab2  4052  cbvopab  4053  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  cbvopab2v  4059  unopab  4061  opabid  4235  elopab  4236  ssopab2  4253  iunopab  4259  elxpi  4620  rabxp  4641  csbxpg  4685  relopabi  4730  opabbrex  5886  dfoprab2  5889  dmoprab  5923  dfopab2  6157  cnvoprab  6202