Definition df-oprab 7416

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 7415 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 7572. (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 7413	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1568	. . . . . . . 8 class 𝑤
8	2	cv 1568	. . . . . . . . . 10 class 𝑥
9	3	cv 1568	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4594	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1568	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4594	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1569	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 400	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1808	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1808	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1808	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2740	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1569	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is used by:  oprabidw  7443  oprabid  7444  dfoprab2  7470  nfoprab1  7473  nfoprab2  7474  nfoprab3  7475  nfoprab  7476  oprabbid  7477  oprabbidv  7478  ssoprab2  7480  0mpo0  7495  mpo0  7497  cbvoprab2  7500  cbvoprab12v  7502  cbvoprab3v  7504  eloprabga  7521  oprabrexex2  7973  eloprabi  8058  dftpos3  8238  join0  18465  meet0  18466  mppspstlem  36071  mppsval  36072  colinearex  36560  cbvoprab1vw  36777  cbvoprab2vw  36778  cbvoprab123vw  36779  cbvoprab23vw  36780  cbvoprab13vw  36781  cbvoprab1davw  36811  cbvoprab2davw  36812  cbvoprab3davw  36813  cbvoprab123davw  36814  cbvoprab12davw  36815  cbvoprab23davw  36816  cbvoprab13davw  36817  csboprabg  38004  eloprab1st2nd  49674