Definition df-opab 4049

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 4047	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1347	. . . . . . 7 class z
7	2	cv 1347	. . . . . . . 8 class x
8	3	cv 1347	. . . . . . . 8 class y
9	7, 8	cop 3584	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1348	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 103	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1485	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1485	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2156	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1348	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4051  opabbid  4052  nfopab  4055  nfopab1  4056  nfopab2  4057  cbvopab  4058  cbvopab1  4060  cbvopab2  4061  cbvopab1s  4062  cbvopab2v  4064  unopab  4066  opabid  4240  elopab  4241  ssopab2  4258  iunopab  4264  elxpi  4625  rabxp  4646  csbxpg  4690  relopabi  4735  opabbrex  5894  dfoprab2  5897  dmoprab  5931  dfopab2  6165  cnvoprab  6210