![]() |
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 6814 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 6959. (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 6812 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
6 | vw | . . . . . . . . 9 setvar 𝑤 | |
7 | 6 | cv 1629 | . . . . . . . 8 class 𝑤 |
8 | 2 | cv 1629 | . . . . . . . . . 10 class 𝑥 |
9 | 3 | cv 1629 | . . . . . . . . . 10 class 𝑦 |
10 | 8, 9 | cop 4325 | . . . . . . . . 9 class 〈𝑥, 𝑦〉 |
11 | 4 | cv 1629 | . . . . . . . . 9 class 𝑧 |
12 | 10, 11 | cop 4325 | . . . . . . . 8 class 〈〈𝑥, 𝑦〉, 𝑧〉 |
13 | 7, 12 | wceq 1630 | . . . . . . 7 wff 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 |
14 | 13, 1 | wa 383 | . . . . . 6 wff (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
15 | 14, 4 | wex 1851 | . . . . 5 wff ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
16 | 15, 3 | wex 1851 | . . . 4 wff ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
17 | 16, 2 | wex 1851 | . . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
18 | 17, 6 | cab 2744 | . 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
19 | 5, 18 | wceq 1630 | 1 wff {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: oprabid 6838 dfoprab2 6864 nfoprab1 6867 nfoprab2 6868 nfoprab3 6869 nfoprab 6870 oprabbid 6871 ssoprab2 6874 mpt20 6888 cbvoprab2 6891 eloprabga 6910 oprabrexex2 7321 eloprabi 7398 dftpos3 7537 meet0 17336 join0 17337 cnvoprabOLD 29805 mppspstlem 31773 mppsval 31774 colinearex 32471 csboprabg 33485 |
Copyright terms: Public domain | W3C validator |