Definition df-oprab 7420

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 7419 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 7576. (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 7417	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1569	. . . . . . . 8 class 𝑤
8	2	cv 1569	. . . . . . . . . 10 class 𝑥
9	3	cv 1569	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4593	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1569	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4593	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1570	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 401	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1812	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1812	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1812	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2740	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1570	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is used by:  oprabidw  7447  oprabid  7448  dfoprab2  7474  nfoprab1  7477  nfoprab2  7478  nfoprab3  7479  nfoprab  7480  oprabbid  7481  oprabbidv  7482  ssoprab2  7484  0mpo0  7499  mpo0  7501  cbvoprab2  7504  cbvoprab12v  7506  cbvoprab3v  7508  eloprabga  7525  oprabrexex2  7978  eloprabi  8063  dftpos3  8245  join0  18495  meet0  18496  mppspstlem  36137  mppsval  36138  colinearex  36627  cbvoprab1vw  36844  cbvoprab2vw  36845  cbvoprab123vw  36846  cbvoprab23vw  36847  cbvoprab13vw  36848  cbvoprab1davw  36878  cbvoprab2davw  36879  cbvoprab3davw  36880  cbvoprab123davw  36881  cbvoprab12davw  36882  cbvoprab23davw  36883  cbvoprab13davw  36884  csboprabg  38071  eloprab1st2nd  49783