Definition df-opab 3810

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

This definition is referenced by:  opabss  3812  opabbid  3813  nfopab  3816  nfopab1  3817  nfopab2  3818  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  unopab  3827  opabid  3985  elopab  3986  ssopab2  4003  iunopab  4009  elxpi  4304  rabxp  4323  csbxpg  4364  relopabi  4406  opabbrex  5491  dfoprab2  5494  dmoprab  5527  dfopab2  5757