Definition df-opab 4149

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 4147	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1394	. . . . . . 7 class z
7	2	cv 1394	. . . . . . . 8 class x
8	3	cv 1394	. . . . . . . 8 class y
9	7, 8	cop 3670	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1395	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 104	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1538	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1538	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2215	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1395	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  4151  opabbid  4152  nfopab  4155  nfopab1  4156  nfopab2  4157  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab2v  4164  unopab  4166  opabid  4348  elopab  4350  ssopab2  4368  iunopab  4374  elxpi  4739  opabssxpd  4760  rabxp  4761  csbxpg  4805  relopabi  4853  opabbrex  6060  dfoprab2  6063  dmoprab  6097  dfopab2  6347  cnvoprab  6394