Definition df-oprab 7357

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 7356 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 7513. (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 7354	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6		vw	. . . . . . . . 9 setvar 𝑤
7	6	cv 1539	. . . . . . . 8 class 𝑤
8	2	cv 1539	. . . . . . . . . 10 class 𝑥
9	3	cv 1539	. . . . . . . . . 10 class 𝑦
10	8, 9	cop 4585	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
11	4	cv 1539	. . . . . . . . 9 class 𝑧
12	10, 11	cop 4585	. . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
13	7, 12	wceq 1540	. . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩
14	13, 1	wa 395	. . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
15	14, 4	wex 1779	. . . . 5 wff ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
16	15, 3	wex 1779	. . . 4 wff ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
17	16, 2	wex 1779	. . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
18	17, 6	cab 2707	. 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
19	5, 18	wceq 1540	1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

This definition is referenced by:  oprabidw  7384  oprabid  7385  dfoprab2  7411  nfoprab1  7414  nfoprab2  7415  nfoprab3  7416  nfoprab  7417  oprabbid  7418  oprabbidv  7419  ssoprab2  7421  0mpo0  7436  mpo0  7438  cbvoprab2  7441  cbvoprab12v  7443  cbvoprab3v  7445  eloprabga  7462  oprabrexex2  7920  eloprabi  8005  dftpos3  8184  join0  18327  meet0  18328  mppspstlem  35546  mppsval  35547  colinearex  36036  cbvoprab1vw  36213  cbvoprab2vw  36214  cbvoprab123vw  36215  cbvoprab23vw  36216  cbvoprab13vw  36217  cbvoprab1davw  36247  cbvoprab2davw  36248  cbvoprab3davw  36249  cbvoprab123davw  36250  cbvoprab12davw  36251  cbvoprab23davw  36252  cbvoprab13davw  36253  csboprabg  37306  eloprab1st2nd  48856