Definition df-opab 3789

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 3787	. 2 class {⟨x, y⟩ ∣ φ}
5		vz	. . . . . . . 8 setvar z
6	5	cv 1225	. . . . . . 7 class z
7	2	cv 1225	. . . . . . . 8 class x
8	3	cv 1225	. . . . . . . 8 class y
9	7, 8	cop 3349	. . . . . . 7 class ⟨x, y⟩
10	6, 9	wceq 1226	. . . . . 6 wff z = ⟨x, y⟩
11	10, 1	wa 97	. . . . 5 wff (z = ⟨x, y⟩ ∧ φ)
12	11, 3	wex 1358	. . . 4 wff ∃y(z = ⟨x, y⟩ ∧ φ)
13	12, 2	wex 1358	. . 3 wff ∃x∃y(z = ⟨x, y⟩ ∧ φ)
14	13, 5	cab 2004	. 2 class {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
15	4, 14	wceq 1226	1 wff {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}

This definition is referenced by:  opabss  3791  opabbid  3792  nfopab  3795  nfopab1  3796  nfopab2  3797  cbvopab  3798  cbvopab1  3800  cbvopab2  3801  cbvopab1s  3802  cbvopab2v  3804  unopab  3806  opabid  3964  elopab  3965  ssopab2  3982  iunopab  3988  elxpi  4284  rabxp  4303  csbxpg  4344  relopabi  4386  opabbrex  5468  dfoprab2  5471  dmoprab  5504  dfopab2  5734