Definition df-opab 4426

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 4711 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 6753. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 25274). (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 4424	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1398	. . . . . . 7 class z
7	2	cv 1398	. . . . . . . 8 class x
8	3	cv 1398	. . . . . . . 8 class y
9	7, 8	cop 3950	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1399	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 367	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1620	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1620	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2367	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1399	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4428  opabbid  4429  nfopab  4432  nfopab1  4433  nfopab2  4434  cbvopab  4435  cbvopab1  4437  cbvopab2  4438  cbvopab1s  4439  cbvopab2v  4441  unopab  4442  opabid  4668  elopab  4669  ssopab2  4687  iunopab  4697  dfid3  4710  elxpi  4929  rabxp  4950  csbxp  4995  relopabi  5040  opabbrexOLD  6239  dfoprab2  6242  dmoprab  6282  opabex2  6637  dfopab2  6753  brdom7disj  8822  brdom6disj  8823  cnvoprab  27696  areacirc  30278  dropab1  31524  dropab2  31525  csbxpgOLD  33964  csbxpgVD  34041  relopabVD  34048