Definition df-opab 2741

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 2915 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 4173.

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 2740	. 2 class {<.x, y>. | ph}
5		vz	. . . . . . . 8 set z
6	5	cv 991	. . . . . . 7 class z
7	2	cv 991	. . . . . . . 8 class x
8	3	cv 991	. . . . . . . 8 class y
9	7, 8	cop 2469	. . . . . . 7 class <.x, y>.
10	6, 9	wceq 992	. . . . . 6 wff z = <.x, y>.
11	10, 1	wa 221	. . . . 5 wff (z = <.x, y>. /\ ph)
12	11, 3	wex 1016	. . . 4 wff E.y(z = <.x, y>. /\ ph)
13	12, 2	wex 1016	. . 3 wff E.xE.y(z = <.x, y>. /\ ph)
14	13, 5	cab 1505	. 2 class {z | E.xE.y(z = <.x, y>. /\ ph)}
15	4, 14	wceq 992	1 wff {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}

This definition is referenced by:  opabss 2742  opabbid 2743  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  cbvopab2v 2751  csbopabg 2752  unopab 2753  opabid 2887  elopab 2888  hbopab1 2890  hbopab2 2891  ssopab2 2900  dfid3 2914  dfoprab2 4050  dmoprab 4062  dfopab2 4173  rdglem2 4239  brdom7disj 4950  brdom6disj 4951  nvvcop 8460  oprabopabf 11807

Copyright terms: Public domain