Definition df-opab 4227

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 (see dfid2 4460 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 6360. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 21693). (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 set x
3		vy	. . 3 set y
4	1, 2, 3	copab 4225	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 set z
6	5	cv 1648	. . . . . . 7 class z
7	2	cv 1648	. . . . . . . 8 class x
8	3	cv 1648	. . . . . . . 8 class y
9	7, 8	cop 3777	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1649	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 359	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1547	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1547	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2390	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1649	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4229  opabbid  4230  nfopab  4233  nfopab1  4234  nfopab2  4235  cbvopab  4236  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  cbvopab2v  4242  unopab  4244  opabid  4421  elopab  4422  ssopab2  4440  iunopab  4446  dfid3  4459  elxpi  4853  csbxpg  4864  rabxp  4873  relopabi  4959  opabbrex  6077  dfoprab2  6080  dmoprab  6113  dfopab2  6360  brdom7disj  8365  brdom6disj  8366  areacirc  26187  dropab1  27517  dropab2  27518  csbxpgVD  28715  relopabVD  28722