![]() |
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 6693 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 the most common operation class builder is given by ovmpt2 6838. (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 6691 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
6 | vw | . . . . . . . . 9 setvar 𝑤 | |
7 | 6 | cv 1522 | . . . . . . . 8 class 𝑤 |
8 | 2 | cv 1522 | . . . . . . . . . 10 class 𝑥 |
9 | 3 | cv 1522 | . . . . . . . . . 10 class 𝑦 |
10 | 8, 9 | cop 4216 | . . . . . . . . 9 class 〈𝑥, 𝑦〉 |
11 | 4 | cv 1522 | . . . . . . . . 9 class 𝑧 |
12 | 10, 11 | cop 4216 | . . . . . . . 8 class 〈〈𝑥, 𝑦〉, 𝑧〉 |
13 | 7, 12 | wceq 1523 | . . . . . . 7 wff 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 |
14 | 13, 1 | wa 383 | . . . . . 6 wff (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
15 | 14, 4 | wex 1744 | . . . . 5 wff ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
16 | 15, 3 | wex 1744 | . . . 4 wff ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
17 | 16, 2 | wex 1744 | . . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
18 | 17, 6 | cab 2637 | . 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
19 | 5, 18 | wceq 1523 | 1 wff {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: oprabid 6717 dfoprab2 6743 nfoprab1 6746 nfoprab2 6747 nfoprab3 6748 nfoprab 6749 oprabbid 6750 ssoprab2 6753 mpt20 6767 cbvoprab2 6770 eloprabga 6789 oprabrexex2 7200 eloprabi 7277 dftpos3 7415 meet0 17184 join0 17185 cnvoprabOLD 29626 mppspstlem 31594 mppsval 31595 colinearex 32292 csboprabg 33306 |
Copyright terms: Public domain | W3C validator |