![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-oprab | Structured version Visualization version GIF version |
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 7415 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 7571. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
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 7413 | . 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 4634 | . . . . . . . . 9 class 〈𝑥, 𝑦〉 |
11 | 4 | cv 1539 | . . . . . . . . 9 class 𝑧 |
12 | 10, 11 | cop 4634 | . . . . . . . 8 class 〈〈𝑥, 𝑦〉, 𝑧〉 |
13 | 7, 12 | wceq 1540 | . . . . . . 7 wff 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 |
14 | 13, 1 | wa 395 | . . . . . 6 wff (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
15 | 14, 4 | wex 1780 | . . . . 5 wff ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
16 | 15, 3 | wex 1780 | . . . 4 wff ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
17 | 16, 2 | wex 1780 | . . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
18 | 17, 6 | cab 2708 | . 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
19 | 5, 18 | wceq 1540 | 1 wff {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: oprabidw 7443 oprabid 7444 dfoprab2 7470 nfoprab1 7473 nfoprab2 7474 nfoprab3 7475 nfoprab 7476 oprabbid 7477 oprabbidv 7478 ssoprab2 7480 0mpo0 7495 mpo0 7497 cbvoprab2 7500 eloprabga 7519 eloprabgaOLD 7520 oprabrexex2 7969 eloprabi 8053 dftpos3 8233 join0 18363 meet0 18364 cnvoprabOLD 32213 mppspstlem 34861 mppsval 34862 colinearex 35337 csboprabg 36515 |
Copyright terms: Public domain | W3C validator |