Definition df-oprab 7424

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 7423 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 7580. (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 7421	. 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 4589	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1568	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4589	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1569	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 401	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1811	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1811	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1811	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2738	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1569	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is used by:  oprabidw  7451  oprabid  7452  dfoprab2  7478  nfoprab1  7481  nfoprab2  7482  nfoprab3  7483  nfoprab  7484  oprabbid  7485  oprabbidv  7486  ssoprab2  7488  0mpo0  7503  mpo0  7505  cbvoprab2  7508  cbvoprab12v  7510  cbvoprab3v  7512  eloprabga  7529  oprabrexex2  7990  eloprabi  8074  dftpos3  8261  join0  18577  meet0  18578  mppspstlem  36378  mppsval  36379  colinearex  36867  cbvoprab1vw  37068  cbvoprab2vw  37069  cbvoprab123vw  37070  cbvoprab23vw  37071  cbvoprab13vw  37072  cbvoprab1davw  37102  cbvoprab2davw  37103  cbvoprab3davw  37104  cbvoprab123davw  37105  cbvoprab12davw  37106  cbvoprab23davw  37107  cbvoprab13davw  37108  csboprabg  38296  eloprab1st2nd  50020