Definition df-opab

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 does not require it (see dfid2 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 . An example is given by ex-opab . (Contributed by NM, 4-Jul-1994)

	Ref	Expression
Assertion	df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2		wph	$$wff\phi$$
3	2 0 1	copab	$$class\left\{⟨x,y⟩|\phi \right\}$$
4		vz	$$setvarz$$
5	4	cv	$$setvarz$$
6	0	cv	$$setvarx$$
7	1	cv	$$setvary$$
8	6 7	cop	$$class⟨x,y⟩$$
9	5 8	wceq	$$wffz=⟨x,y⟩$$
10	9 2	wa	$$wff\left(z=⟨x,y⟩\wedge \phi \right)$$
11	10 1	wex	$$wff\exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
12	11 0	wex	$$wff\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
13	12 4	cab	$$class\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
14	3 13	wceq	$$wff\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$