Definition df-opab 4145

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 4143	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1394	. . . . . . 7 class z
7	2	cv 1394	. . . . . . . 8 class x
8	3	cv 1394	. . . . . . . 8 class y
9	7, 8	cop 3669	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1395	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 104	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1538	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1538	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2215	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1395	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4147  opabbid  4148  nfopab  4151  nfopab1  4152  nfopab2  4153  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab2v  4160  unopab  4162  opabid  4343  elopab  4345  ssopab2  4363  iunopab  4369  elxpi  4734  rabxp  4755  csbxpg  4799  relopabi  4846  opabbrex  6047  dfoprab2  6050  dmoprab  6084  dfopab2  6333  cnvoprab  6378