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 5147 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 7158 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1536 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 2114 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1536 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 2114 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 398 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1536 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1537 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 398 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 7157 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1537 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpoeq123 7226 mpoeq123dva 7228 mpoeq3dva 7231 nfmpo1 7234 nfmpo2 7235 nfmpo 7236 0mpo0 7237 mpo0 7239 cbvmpox 7247 mpov 7264 mpomptx 7265 resmpo 7272 mpofun 7276 mpo2eqb 7283 rnmpo 7284 reldmmpo 7285 elrnmpores 7288 ovmpt4g 7297 mpondm0 7386 elmpocl 7387 fmpox 7765 bropopvvv 7785 bropfvvvv 7787 tposmpo 7929 erovlem 8393 xpcomco 8607 omxpenlem 8618 cpnnen 15582 mpomptxf 30425 df1stres 30439 df2ndres 30440 f1od2 30457 sxbrsigalem5 31546 dmscut 33272 bj-dfmpoa 34413 csbmpo123 34615 uncf 34886 unccur 34890 mpobi123f 35455 cbvmpo2 41412 cbvmpo1 41413 mpomptx2 44432 cbvmpox2 44433 |
Copyright terms: Public domain | W3C validator |