Definition df-opab 4483

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 4771 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 25880). (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 4481	. 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 4004	. . . . . . 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 1657	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1657	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2407	. 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  4485  opabbid  4486  nfopab  4489  nfopab1  4490  nfopab2  4491  cbvopab  4492  cbvopab1  4494  cbvopab2  4495  cbvopab1s  4496  cbvopab2v  4498  unopab  4499  opabid  4727  elopab  4728  ssopab2  4746  iunopab  4756  dfid3  4769  elxpi  4869  rabxp  4890  csbxp  4935  relopabi  4978  opabbrexOLD  6348  dfoprab2  6351  dmoprab  6391  opabex2  6745  dfopab2  6861  brdom7disj  8966  brdom6disj  8967  cnvoprab  28314  areacirc  32001  dropab1  36770  dropab2  36771  csbxpgOLD  37187  csbxpgVD  37264  relopabVD  37271