Definition df-opab 3930

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 3928	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1298	. . . . . . 7 class z
7	2	cv 1298	. . . . . . . 8 class x
8	3	cv 1298	. . . . . . . 8 class y
9	7, 8	cop 3477	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1299	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 103	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1436	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1436	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2086	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1299	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  3932  opabbid  3933  nfopab  3936  nfopab1  3937  nfopab2  3938  cbvopab  3939  cbvopab1  3941  cbvopab2  3942  cbvopab1s  3943  cbvopab2v  3945  unopab  3947  opabid  4117  elopab  4118  ssopab2  4135  iunopab  4141  elxpi  4493  rabxp  4514  csbxpg  4558  relopabi  4603  opabbrex  5747  dfoprab2  5750  dmoprab  5784  dfopab2  6017  cnvoprab  6061