Definition df-oprab 7418

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 7417 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 7574. (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 7415	. 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 4590	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1569	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4590	. . . . . . . 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 2738	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1570	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is used by:  oprabidw  7445  oprabid  7446  dfoprab2  7472  nfoprab1  7475  nfoprab2  7476  nfoprab3  7477  nfoprab  7478  oprabbid  7479  oprabbidv  7480  ssoprab2  7482  0mpo0  7497  mpo0  7499  cbvoprab2  7502  cbvoprab12v  7504  cbvoprab3v  7506  eloprabga  7523  oprabrexex2  7976  eloprabi  8061  dftpos3  8243  join0  18494  meet0  18495  mppspstlem  36153  mppsval  36154  colinearex  36643  cbvoprab1vw  36860  cbvoprab2vw  36861  cbvoprab123vw  36862  cbvoprab23vw  36863  cbvoprab13vw  36864  cbvoprab1davw  36894  cbvoprab2davw  36895  cbvoprab3davw  36896  cbvoprab123davw  36897  cbvoprab12davw  36898  cbvoprab23davw  36899  cbvoprab13davw  36900  csboprabg  38087  eloprab1st2nd  49799