Definition df-opab 3846

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 3844	. 2 class { <. x , y >. | ph }
5		vz	. . . . . . . 8 setvar z
6	5	cv 1258	. . . . . . 7 class z
7	2	cv 1258	. . . . . . . 8 class x
8	3	cv 1258	. . . . . . . 8 class y
9	7, 8	cop 3405	. . . . . . 7 class <. x , y >.
10	6, 9	wceq 1259	. . . . . 6 wff z = <. x , y >.
11	10, 1	wa 101	. . . . 5 wff ( z = <. x , y >. /\ ph )
12	11, 3	wex 1397	. . . 4 wff E. y ( z = <. x , y >. /\ ph )
13	12, 2	wex 1397	. . 3 wff E. x E. y ( z = <. x , y >. /\ ph )
14	13, 5	cab 2042	. 2 class { z | E. x E. y ( z = <. x , y >. /\ ph ) }
15	4, 14	wceq 1259	1 wff { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

This definition is referenced by:  opabss  3848  opabbid  3849  nfopab  3852  nfopab1  3853  nfopab2  3854  cbvopab  3855  cbvopab1  3857  cbvopab2  3858  cbvopab1s  3859  cbvopab2v  3861  unopab  3863  opabid  4021  elopab  4022  ssopab2  4039  iunopab  4045  elxpi  4388  rabxp  4407  csbxpg  4448  relopabi  4490  opabbrex  5576  dfoprab2  5579  dmoprab  5612  dfopab2  5842  cnvoprab  5882