Definition df-oprab 7360

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 7359 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 7516. (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 7357	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1541	. . . . . . . 8 class 𝑤
8	2	cv 1541	. . . . . . . . . 10 class 𝑥
9	3	cv 1541	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4563	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1541	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4563	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1542	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 395	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1781	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1781	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1781	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2713	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1542	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is referenced by:  oprabidw  7387  oprabid  7388  dfoprab2  7414  nfoprab1  7417  nfoprab2  7418  nfoprab3  7419  nfoprab  7420  oprabbid  7421  oprabbidv  7422  ssoprab2  7424  0mpo0  7439  mpo0  7441  cbvoprab2  7444  cbvoprab12v  7446  cbvoprab3v  7448  eloprabga  7465  oprabrexex2  7920  eloprabi  8005  dftpos3  8183  join0  18358  meet0  18359  mppspstlem  35741  mppsval  35742  colinearex  36230  cbvoprab1vw  36407  cbvoprab2vw  36408  cbvoprab123vw  36409  cbvoprab23vw  36410  cbvoprab13vw  36411  cbvoprab1davw  36441  cbvoprab2davw  36442  cbvoprab3davw  36443  cbvoprab123davw  36444  cbvoprab12davw  36445  cbvoprab23davw  36446  cbvoprab13davw  36447  csboprabg  37634  eloprab1st2nd  49331