Definition df-opab 3861

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

This definition is referenced by:  opabss  3863  opabbid  3864  nfopab  3867  nfopab1  3868  nfopab2  3869  cbvopab  3870  cbvopab1  3872  cbvopab2  3873  cbvopab1s  3874  cbvopab2v  3876  unopab  3878  opabid  4041  elopab  4042  ssopab2  4059  iunopab  4065  elxpi  4408  rabxp  4427  csbxpg  4468  relopabi  4512  opabbrex  5602  dfoprab2  5605  dmoprab  5638  dfopab2  5868  cnvoprab  5908