Definition df-opab 4077

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. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (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 4075	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1362	. . . . . . 7 class z
7	2	cv 1362	. . . . . . . 8 class x
8	3	cv 1362	. . . . . . . 8 class y
9	7, 8	cop 3607	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1363	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 104	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1502	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1502	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2173	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1363	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4079  opabbid  4080  nfopab  4083  nfopab1  4084  nfopab2  4085  cbvopab  4086  cbvopab1  4088  cbvopab2  4089  cbvopab1s  4090  cbvopab2v  4092  unopab  4094  opabid  4269  elopab  4270  ssopab2  4287  iunopab  4293  elxpi  4654  rabxp  4675  csbxpg  4719  relopabi  4764  opabbrex  5932  dfoprab2  5935  dmoprab  5969  dfopab2  6204  cnvoprab  6249