Definition df-oprab 7434

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 7433 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 an operation given by a class abstraction is given by ovmpo 7592. (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 7431	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1535	. . . . . . . 8 class 𝑤
8	2	cv 1535	. . . . . . . . . 10 class 𝑥
9	3	cv 1535	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4636	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1535	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4636	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1536	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 395	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1775	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1775	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1775	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2711	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1536	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is referenced by:  oprabidw  7461  oprabid  7462  dfoprab2  7490  nfoprab1  7493  nfoprab2  7494  nfoprab3  7495  nfoprab  7496  oprabbid  7497  oprabbidv  7498  ssoprab2  7500  0mpo0  7515  mpo0  7517  cbvoprab2  7520  cbvoprab12v  7522  cbvoprab3v  7524  eloprabga  7540  eloprabgaOLD  7541  oprabrexex2  8001  eloprabi  8086  dftpos3  8267  join0  18462  meet0  18463  cnvoprabOLD  32737  mppspstlem  35555  mppsval  35556  colinearex  36041  cbvoprab1vw  36219  cbvoprab2vw  36220  cbvoprab123vw  36221  cbvoprab23vw  36222  cbvoprab13vw  36223  cbvoprab1davw  36253  cbvoprab2davw  36254  cbvoprab3davw  36255  cbvoprab123davw  36256  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  csboprabg  37312