Definition df-oprab 7452

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 7451 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 7610. (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 7449	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1536	. . . . . . . 8 class 𝑤
8	2	cv 1536	. . . . . . . . . 10 class 𝑥
9	3	cv 1536	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4654	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1536	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4654	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1537	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 395	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1777	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1777	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1777	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2717	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1537	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is referenced by:  oprabidw  7479  oprabid  7480  dfoprab2  7508  nfoprab1  7511  nfoprab2  7512  nfoprab3  7513  nfoprab  7514  oprabbid  7515  oprabbidv  7516  ssoprab2  7518  0mpo0  7533  mpo0  7535  cbvoprab2  7538  cbvoprab12v  7540  cbvoprab3v  7542  eloprabga  7558  eloprabgaOLD  7559  oprabrexex2  8019  eloprabi  8104  dftpos3  8285  join0  18475  meet0  18476  cnvoprabOLD  32734  mppspstlem  35539  mppsval  35540  colinearex  36024  cbvoprab1vw  36203  cbvoprab2vw  36204  cbvoprab123vw  36205  cbvoprab23vw  36206  cbvoprab13vw  36207  cbvoprab1davw  36237  cbvoprab2davw  36238  cbvoprab3davw  36239  cbvoprab123davw  36240  cbvoprab12davw  36241  cbvoprab23davw  36242  cbvoprab13davw  36243  csboprabg  37296