Definition df-oprab 5529

Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 5527 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)

Assertion

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

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

Allowed substitution hints:   φ(x,y,z)

Detailed syntax breakdown of Definition df-oprab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		vz	. . 3 setvar z
5	1, 2, 3, 4	coprab 5528	. 2 class {⟨⟨x, y⟩, z⟩ ∣ φ}
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1641	. . . . . . . 8 class w
8	2	cv 1641	. . . . . . . . . 10 class x
9	3	cv 1641	. . . . . . . . . 10 class y
10	8, 9	cop 4562	. . . . . . . . 9 class ⟨x, y⟩
11	4	cv 1641	. . . . . . . . 9 class z
12	10, 11	cop 4562	. . . . . . . 8 class ⟨⟨x, y⟩, z⟩
13	7, 12	wceq 1642	. . . . . . 7 wff w = ⟨⟨x, y⟩, z⟩
14	13, 1	wa 358	. . . . . 6 wff (w = ⟨⟨x, y⟩, z⟩ ∧ φ)
15	14, 4	wex 1541	. . . . 5 wff ∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)
16	15, 3	wex 1541	. . . 4 wff ∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)
17	16, 2	wex 1541	. . 3 wff ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)
18	17, 6	cab 2339	. 2 class {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
19	5, 18	wceq 1642	1 wff {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}

This definition is referenced by:  nfoprab1  5547  nfoprab2  5548  nfoprab3  5549  nfoprab  5550  oprabid  5551  dfoprab2  5559  hboprab1  5560  hboprab2  5561  hboprab3  5562  hboprab  5563  oprabbid  5564  cbvoprab2  5569  eloprabga  5579