| 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 7434 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 7593. (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 7432 | . 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 4632 | . . . . . . . . 9 class 〈𝑥, 𝑦〉 |
| 11 | 4 | cv 1539 | . . . . . . . . 9 class 𝑧 |
| 12 | 10, 11 | cop 4632 | . . . . . . . 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 2714 | . 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
| 19 | 5, 18 | wceq 1540 | 1 wff {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: oprabidw 7462 oprabid 7463 dfoprab2 7491 nfoprab1 7494 nfoprab2 7495 nfoprab3 7496 nfoprab 7497 oprabbid 7498 oprabbidv 7499 ssoprab2 7501 0mpo0 7516 mpo0 7518 cbvoprab2 7521 cbvoprab12v 7523 cbvoprab3v 7525 eloprabga 7542 oprabrexex2 8003 eloprabi 8088 dftpos3 8269 join0 18450 meet0 18451 mppspstlem 35576 mppsval 35577 colinearex 36061 cbvoprab1vw 36238 cbvoprab2vw 36239 cbvoprab123vw 36240 cbvoprab23vw 36241 cbvoprab13vw 36242 cbvoprab1davw 36272 cbvoprab2davw 36273 cbvoprab3davw 36274 cbvoprab123davw 36275 cbvoprab12davw 36276 cbvoprab23davw 36277 cbvoprab13davw 36278 csboprabg 37331 |
| Copyright terms: Public domain | W3C validator |