Definition df-opab 3396

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 (see dfid2 3588 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 5053.

Assertion

Ref	Expression
df-opab	|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}

Distinct variable groups:   x,z   y,z   ph,z

Detailed syntax breakdown of Definition df-opab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3		vy	. . 3 set y
4	1, 2, 3	copab 3395	. 2 class {<.x, y>. | ph}
5		vz	. . . . . . . 8 set z
6	5	cv 1297	. . . . . . 7 class z
7	2	cv 1297	. . . . . . . 8 class x
8	3	cv 1297	. . . . . . . 8 class y
9	7, 8	cop 3046	. . . . . . 7 class <.x, y>.
10	6, 9	wceq 1298	. . . . . 6 wff z = <.x, y>.
11	10, 1	wa 240	. . . . 5 wff (z = <.x, y>. /\ ph)
12	11, 3	wex 1326	. . . 4 wff E.y(z = <.x, y>. /\ ph)
13	12, 2	wex 1326	. . 3 wff E.xE.y(z = <.x, y>. /\ ph)
14	13, 5	cab 1871	. 2 class {z | E.xE.y(z = <.x, y>. /\ ph)}
15	4, 14	wceq 1298	1 wff {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}

This definition is referenced by:  opabss 3397  opabssOLD 3398  opabbid 3399  opabbidOLD 3400  cbvopab 3403  cbvopab1 3405  cbvopab1s 3406  cbvopab2v 3408  csbopabg 3409  unopab 3410  opabid 3557  opabidOLD 3558  elopab 3559  hbopab 3560  hbopab1 3562  hbopab2 3563  ssopab2 3573  dfid3 3587  iunfopab 4542  dfoprab2 4917  dmoprab 4931  dfopab2 5053  rdglem2 5146  brdom7disj 5966  brdom6disj 5967  nvvcop 9545  oprabopabf 10157  dropab1 16424  dropab2 16425

Copyright terms: Public domain