| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-mpo | Structured version Visualization version GIF version | ||
| Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)". An extension of df-mpt 5226 for two arguments. (Contributed by NM, 17-Feb-2008.) |
| Ref | Expression |
|---|---|
| df-mpo | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx | . . 3 setvar 𝑥 | |
| 2 | vy | . . 3 setvar 𝑦 | |
| 3 | cA | . . 3 class 𝐴 | |
| 4 | cB | . . 3 class 𝐵 | |
| 5 | cC | . . 3 class 𝐶 | |
| 6 | 1, 2, 3, 4, 5 | cmpo 7433 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| 7 | 1 | cv 1539 | . . . . . 6 class 𝑥 |
| 8 | 7, 3 | wcel 2108 | . . . . 5 wff 𝑥 ∈ 𝐴 |
| 9 | 2 | cv 1539 | . . . . . 6 class 𝑦 |
| 10 | 9, 4 | wcel 2108 | . . . . 5 wff 𝑦 ∈ 𝐵 |
| 11 | 8, 10 | wa 395 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
| 12 | vz | . . . . . 6 setvar 𝑧 | |
| 13 | 12 | cv 1539 | . . . . 5 class 𝑧 |
| 14 | 13, 5 | wceq 1540 | . . . 4 wff 𝑧 = 𝐶 |
| 15 | 11, 14 | wa 395 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
| 16 | 15, 1, 2, 12 | coprab 7432 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| 17 | 6, 16 | wceq 1540 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: mpoeq123 7505 mpoeq123dva 7507 mpoeq3dva 7510 nfmpo1 7513 nfmpo2 7514 nfmpo 7515 0mpo0 7516 mpo0 7518 cbvmpox 7526 cbvmpov 7528 mpov 7545 mpomptx 7546 resmpo 7553 mpofun 7557 mpo2eqb 7565 rnmpo 7566 reldmmpo 7567 elrnmpores 7571 ovmpt4g 7580 mpondm0 7673 elmpocl 7674 fmpox 8092 bropopvvv 8115 bropfvvvv 8117 tposmpo 8288 erovlem 8853 xpcomco 9102 omxpenlem 9113 mpoaddf 11249 mpomulf 11250 cpnnen 16265 dmscut 27856 mpomptxf 32687 df1stres 32713 df2ndres 32714 f1od2 32732 sxbrsigalem5 34290 cbvmpovw2 36243 cbvmpo1vw2 36244 cbvmpo2vw2 36245 cbvmpodavw2 36292 cbvmpo1davw2 36293 cbvmpo2davw2 36294 bj-dfmpoa 37119 csbmpo123 37332 uncf 37606 unccur 37610 mpobi123f 38169 cbvmpo2 45102 cbvmpo1 45103 mpomptx2 48251 cbvmpox2 48252 |
| Copyright terms: Public domain | W3C validator |