Definition df-opab 2673

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 2844 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 4120.

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

This definition is referenced by:  opabss 2674  opabbid 2675  cbvopab 2678  cbvopab1 2680  cbvopab1s 2681  cbvopab2v 2683  csbopabg 2684  unopab 2685  opabid 2817  elopab 2818  hbopab1 2820  hbopab2 2821  ssopab2 2829  dfid3 2843  rdglem2 3945  dfoprab2 3998  dmoprab 4009  dfopab2 4120  brdom7disj 4821  brdom6disj 4822  nvvcop 8216

Copyright terms: Public domain