Definition df-opab 4496

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 4787 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 6839. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 25131). (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 4494	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1382	. . . . . . 7 class z
7	2	cv 1382	. . . . . . . 8 class x
8	3	cv 1382	. . . . . . . 8 class y
9	7, 8	cop 4020	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1383	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 369	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1599	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1599	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2428	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1383	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4498  opabbid  4499  nfopab  4502  nfopab1  4503  nfopab2  4504  cbvopab  4505  cbvopab1  4507  cbvopab2  4508  cbvopab1s  4509  cbvopab2v  4511  unopab  4512  opabid  4744  elopab  4745  ssopab2  4763  iunopab  4773  dfid3  4786  elxpi  5005  rabxp  5026  csbxp  5071  csbxpgOLD  5072  relopabi  5118  opabbrexOLD  6325  dfoprab2  6328  dmoprab  6368  opabex2  6723  dfopab2  6839  brdom7disj  8912  brdom6disj  8913  swrd0  12640  cnvoprab  27524  areacirc  30088  dropab1  31310  dropab2  31311  csbxpgVD  33562  relopabVD  33569