Definition df-opab 4501

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 4792 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 6830. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 24818). (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 4499	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1373	. . . . . . 7 class z
7	2	cv 1373	. . . . . . . 8 class x
8	3	cv 1373	. . . . . . . 8 class y
9	7, 8	cop 4028	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1374	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 369	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1591	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1591	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2447	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1374	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4503  opabbid  4504  nfopab  4507  nfopab1  4508  nfopab2  4509  cbvopab  4510  cbvopab1  4512  cbvopab2  4513  cbvopab1s  4514  cbvopab2v  4516  unopab  4517  opabid  4749  elopab  4750  ssopab2  4768  iunopab  4778  dfid3  4791  elxpi  5010  rabxp  5030  csbxp  5074  csbxpgOLD  5075  relopabi  5121  opabbrex  6317  dfoprab2  6320  dmoprab  6360  opabex2  6714  dfopab2  6830  brdom7disj  8900  brdom6disj  8901  swrd0  12610  cnvoprab  27206  areacirc  29678  dropab1  30891  dropab2  30892  csbxpgVD  32651  relopabVD  32658