Definition df-opab 4624

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 4770 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 4623	. 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 4562	. . . . . . 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  4625  nfopab  4628  nfopab1  4629  nfopab2  4630  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab2v  4637  unopab  4639  opabid  4696  elopab  4697  ssopab2  4713  dfid3  4769  elxpi  4801  csbxpg  4814  rabxp  4815  iunfopab  5205  dfoprab2  5559  dmoprab  5575