Definition df-opab 2662

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 2832 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 4103.

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

This definition is referenced by:  opabss 2663  opabbid 2664  cbvopab 2667  cbvopab1 2669  cbvopab1s 2670  cbvopab2v 2672  csbopabg 2673  unopab 2674  opabid 2805  elopab 2806  hbopab1 2808  hbopab2 2809  ssopab2 2817  dfid3 2831  rdglem2 3929  dfoprab2 3982  dmoprab 3993  dfopab2 4103  brdom7disj 4784  brdom6disj 4785  nvvcop 8165

Copyright terms: Public domain