Definition df-opab 2667

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 2837 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 4113.

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 2666	. 2 class {<.x, y>. | ph}
5		vz	. . . . . . . 8 set z
6	5	cv 955	. . . . . . 7 class z
7	2	cv 955	. . . . . . . 8 class x
8	3	cv 955	. . . . . . . 8 class y
9	7, 8	cop 2411	. . . . . . 7 class <.x, y>.
10	6, 9	wceq 956	. . . . . 6 wff z = <.x, y>.
11	10, 1	wa 223	. . . . 5 wff (z = <.x, y>. /\ ph)
12	11, 3	wex 980	. . . 4 wff E.y(z = <.x, y>. /\ ph)
13	12, 2	wex 980	. . 3 wff E.xE.y(z = <.x, y>. /\ ph)
14	13, 5	cab 1463	. 2 class {z | E.xE.y(z = <.x, y>. /\ ph)}
15	4, 14	wceq 956	1 wff {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}

This definition is referenced by:  opabss 2668  opabbid 2669  cbvopab 2672  cbvopab1 2674  cbvopab1s 2675  cbvopab2v 2677  csbopabg 2678  unopab 2679  opabid 2810  elopab 2811  hbopab1 2813  hbopab2 2814  ssopab2 2822  dfid3 2836  rdglem2 3938  dfoprab2 3991  dmoprab 4002  dfopab2 4113  brdom7disj 4804  brdom6disj 4805  nvvcop 8213

Copyright terms: Public domain