Definition df-oprab 7444

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

This definition is used by:  oprabidw  7471  oprabid  7472  dfoprab2  7498  nfoprab1  7501  nfoprab2  7502  nfoprab3  7503  nfoprab  7504  oprabbid  7505  oprabbidv  7506  ssoprab2  7508  0mpo0  7523  mpo0  7525  cbvoprab2  7528  cbvoprab12v  7530  cbvoprab3v  7532  eloprabga  7549  oprabrexex2  8011  eloprabi  8096  dftpos3  8286  join0  18603  meet0  18604  mppspstlem  36502  mppsval  36503  colinearex  37002  cbvoprab1vw  37203  cbvoprab2vw  37204  cbvoprab123vw  37205  cbvoprab23vw  37206  cbvoprab13vw  37207  cbvoprab1davw  37237  cbvoprab2davw  37238  cbvoprab3davw  37239  cbvoprab123davw  37240  cbvoprab12davw  37241  cbvoprab23davw  37242  cbvoprab13davw  37243  csboprabg  38444  eloprab1st2nd  50182