Definition df-opab 4623

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 4769 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. (Contributed by SF, 12-Jan-2015.)

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 4622	. 2 class {⟨x, y⟩ ∣ φ}
5		vz	. . . . . . . 8 setvar z
6	5	cv 1641	. . . . . . 7 class z
7	2	cv 1641	. . . . . . . 8 class x
8	3	cv 1641	. . . . . . . 8 class y
9	7, 8	cop 4561	. . . . . . 7 class ⟨x, y⟩
10	6, 9	wceq 1642	. . . . . 6 wff z = ⟨x, y⟩
11	10, 1	wa 358	. . . . 5 wff (z = ⟨x, y⟩ ∧ φ)
12	11, 3	wex 1541	. . . 4 wff ∃y(z = ⟨x, y⟩ ∧ φ)
13	12, 2	wex 1541	. . 3 wff ∃x∃y(z = ⟨x, y⟩ ∧ φ)
14	13, 5	cab 2339	. 2 class {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
15	4, 14	wceq 1642	1 wff {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}

This definition is referenced by:  opabbid  4624  nfopab  4627  nfopab1  4628  nfopab2  4629  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  unopab  4638  opabid  4695  elopab  4696  ssopab2  4712  dfid3  4768  elxpi  4800  csbxpg  4813  rabxp  4814  iunfopab  5204  dfoprab2  5558  dmoprab  5574