Definition df-opab 4485

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 4772 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 6861. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 25727). (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 4483	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1436	. . . . . . 7 class z
7	2	cv 1436	. . . . . . . 8 class x
8	3	cv 1436	. . . . . . . 8 class y
9	7, 8	cop 4008	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1437	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 370	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1659	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1659	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2414	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1437	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4487  opabbid  4488  nfopab  4491  nfopab1  4492  nfopab2  4493  cbvopab  4494  cbvopab1  4496  cbvopab2  4497  cbvopab1s  4498  cbvopab2v  4500  unopab  4501  opabid  4728  elopab  4729  ssopab2  4747  iunopab  4757  dfid3  4770  elxpi  4870  rabxp  4891  csbxp  4936  relopabi  4979  opabbrexOLD  6348  dfoprab2  6351  dmoprab  6391  opabex2  6745  dfopab2  6861  brdom7disj  8957  brdom6disj  8958  cnvoprab  28151  areacirc  31740  dropab1  36436  dropab2  36437  csbxpgOLD  36853  csbxpgVD  36930  relopabVD  36937