Definition df-opab 4478

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 4774 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 6879. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 25938). (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 4476	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1454	. . . . . . 7 class z
7	2	cv 1454	. . . . . . . 8 class x
8	3	cv 1454	. . . . . . . 8 class y
9	7, 8	cop 3986	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1455	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 375	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1674	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1674	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2448	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1455	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4480  opabbid  4481  nfopab  4484  nfopab1  4485  nfopab2  4486  cbvopab  4487  cbvopab1  4489  cbvopab2  4490  cbvopab1s  4491  cbvopab2v  4493  unopab  4494  opabid  4725  elopab  4726  ssopab2  4744  iunopab  4754  dfid3  4772  elxpi  4872  rabxp  4893  csbxp  4938  relopabi  4981  opabbrexOLD  6363  dfoprab2  6369  dmoprab  6409  opabex2  6763  dfopab2  6879  brdom7disj  8990  brdom6disj  8991  cnvoprab  28360  areacirc  32083  dropab1  36845  dropab2  36846  csbxpgOLD  37255  csbxpgVD  37332  relopabVD  37339