Definition df-opab 4038

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 4036	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1341	. . . . . . 7 class z
7	2	cv 1341	. . . . . . . 8 class x
8	3	cv 1341	. . . . . . . 8 class y
9	7, 8	cop 3573	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1342	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 103	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1479	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1479	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2150	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1342	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4040  opabbid  4041  nfopab  4044  nfopab1  4045  nfopab2  4046  cbvopab  4047  cbvopab1  4049  cbvopab2  4050  cbvopab1s  4051  cbvopab2v  4053  unopab  4055  opabid  4229  elopab  4230  ssopab2  4247  iunopab  4253  elxpi  4614  rabxp  4635  csbxpg  4679  relopabi  4724  opabbrex  5877  dfoprab2  5880  dmoprab  5914  dfopab2  6149  cnvoprab  6193