Definition df-oprab 6815

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 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 6814 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 ovmpt2 6959. (Contributed by NM, 12-Mar-1995.)

Assertion

Ref	Expression
df-oprab	⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

Distinct variable groups:   𝑥,𝑤   𝑦,𝑤   𝑧,𝑤   𝜑,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Definition df-oprab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		vz	. . 3 setvar 𝑧
5	1, 2, 3, 4	coprab 6812	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1629	. . . . . . . 8 class 𝑤
8	2	cv 1629	. . . . . . . . . 10 class 𝑥
9	3	cv 1629	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4325	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1629	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4325	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1630	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 383	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1851	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1851	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1851	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2744	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1630	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is referenced by:  oprabid  6838  dfoprab2  6864  nfoprab1  6867  nfoprab2  6868  nfoprab3  6869  nfoprab  6870  oprabbid  6871  ssoprab2  6874  mpt20  6888  cbvoprab2  6891  eloprabga  6910  oprabrexex2  7321  eloprabi  7398  dftpos3  7537  meet0  17336  join0  17337  cnvoprabOLD  29805  mppspstlem  31773  mppsval  31774  colinearex  32471  csboprabg  33485