Definition df-opab 4105

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

This definition is referenced by:  opabss  4107  opabbid  4108  nfopab  4111  nfopab1  4112  nfopab2  4113  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  cbvopab2v  4120  unopab  4122  opabid  4301  elopab  4303  ssopab2  4321  iunopab  4327  elxpi  4690  rabxp  4711  csbxpg  4755  relopabi  4802  opabbrex  5988  dfoprab2  5991  dmoprab  6025  dfopab2  6274  cnvoprab  6319