Definition df-opab 4156

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 4154	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1397	. . . . . . 7 class z
7	2	cv 1397	. . . . . . . 8 class x
8	3	cv 1397	. . . . . . . 8 class y
9	7, 8	cop 3676	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1398	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 104	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1541	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1541	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2217	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1398	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4158  opabbid  4159  nfopab  4162  nfopab1  4163  nfopab2  4164  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  unopab  4173  opabid  4356  elopab  4358  ssopab2  4376  iunopab  4382  elxpi  4747  opabssxpd  4768  rabxp  4769  csbxpg  4813  relopabi  4861  opabbrex  6075  dfoprab2  6078  dmoprab  6112  dfopab2  6361  cnvoprab  6408