Definition df-opab 4117

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 4115	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1372	. . . . . . 7 class z
7	2	cv 1372	. . . . . . . 8 class x
8	3	cv 1372	. . . . . . . 8 class y
9	7, 8	cop 3641	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1373	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 104	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1516	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1516	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2192	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1373	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4119  opabbid  4120  nfopab  4123  nfopab1  4124  nfopab2  4125  cbvopab  4126  cbvopab1  4128  cbvopab2  4129  cbvopab1s  4130  cbvopab2v  4132  unopab  4134  opabid  4315  elopab  4317  ssopab2  4335  iunopab  4341  elxpi  4704  rabxp  4725  csbxpg  4769  relopabi  4816  opabbrex  6007  dfoprab2  6010  dmoprab  6044  dfopab2  6293  cnvoprab  6338