Definition df-opab 3783

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. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-opab	⊢ {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}

Distinct variable groups:   x,z   y,z   φ,z

Allowed substitution hints:   φ(x,y)

Detailed syntax breakdown of Definition df-opab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4	1, 2, 3	copab 3781	. 2 class {⟨x, y⟩ ∣ φ}
5		vz	. . . . . . . 8 setvar z
6	5	cv 1223	. . . . . . 7 class z
7	2	cv 1223	. . . . . . . 8 class x
8	3	cv 1223	. . . . . . . 8 class y
9	7, 8	cop 3343	. . . . . . 7 class ⟨x, y⟩
10	6, 9	wceq 1224	. . . . . 6 wff z = ⟨x, y⟩
11	10, 1	wa 97	. . . . 5 wff (z = ⟨x, y⟩ ∧ φ)
12	11, 3	wex 1355	. . . 4 wff ∃y(z = ⟨x, y⟩ ∧ φ)
13	12, 2	wex 1355	. . 3 wff ∃x∃y(z = ⟨x, y⟩ ∧ φ)
14	13, 5	cab 2000	. 2 class {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
15	4, 14	wceq 1224	1 wff {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}

This definition is referenced by:  opabss  3785  opabbid  3786  nfopab  3789  nfopab1  3790  nfopab2  3791  cbvopab  3792  cbvopab1  3794  cbvopab2  3795  cbvopab1s  3796  cbvopab2v  3798  unopab  3800  opabid  3958  elopab  3959  ssopab2  3976  iunopab  3982  elxpi  4277  rabxp  4296  csbxpg  4337  relopabi  4379  opabbrex  5461  dfoprab2  5464  dmoprab  5497  dfopab2  5727