Definition df-opab 3840

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 3838	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1283	. . . . . . 7 class z
7	2	cv 1283	. . . . . . . 8 class x
8	3	cv 1283	. . . . . . . 8 class y
9	7, 8	cop 3401	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1284	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 102	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1421	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1421	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2067	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1284	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  3842  opabbid  3843  nfopab  3846  nfopab1  3847  nfopab2  3848  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab2v  3855  unopab  3857  opabid  4012  elopab  4013  ssopab2  4030  iunopab  4036  elxpi  4379  rabxp  4398  csbxpg  4439  relopabi  4481  opabbrex  5569  dfoprab2  5572  dmoprab  5605  dfopab2  5835  cnvoprab  5875