![]() |
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 5225 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 7395 | . 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
7 | 1 | cv 1540 | . . . . . 6 class 𝑥 |
8 | 7, 3 | wcel 2106 | . . . . 5 wff 𝑥 ∈ 𝐴 |
9 | 2 | cv 1540 | . . . . . 6 class 𝑦 |
10 | 9, 4 | wcel 2106 | . . . . 5 wff 𝑦 ∈ 𝐵 |
11 | 8, 10 | wa 396 | . . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
12 | vz | . . . . . 6 setvar 𝑧 | |
13 | 12 | cv 1540 | . . . . 5 class 𝑧 |
14 | 13, 5 | wceq 1541 | . . . 4 wff 𝑧 = 𝐶 |
15 | 11, 14 | wa 396 | . . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
16 | 15, 1, 2, 12 | coprab 7394 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
17 | 6, 16 | wceq 1541 | 1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpoeq123 7465 mpoeq123dva 7467 mpoeq3dva 7470 nfmpo1 7473 nfmpo2 7474 nfmpo 7475 0mpo0 7476 mpo0 7478 cbvmpox 7486 mpov 7504 mpomptx 7505 resmpo 7512 mpofun 7516 mpofunOLD 7517 mpo2eqb 7524 rnmpo 7525 reldmmpo 7526 elrnmpores 7529 ovmpt4g 7538 mpondm0 7630 elmpocl 7631 fmpox 8035 bropopvvv 8058 bropfvvvv 8060 tposmpo 8230 erovlem 8790 xpcomco 9045 omxpenlem 9056 cpnnen 16154 dmscut 27238 mpomptxf 31775 df1stres 31796 df2ndres 31797 f1od2 31817 sxbrsigalem5 33118 bj-dfmpoa 35803 csbmpo123 36016 uncf 36271 unccur 36275 mpobi123f 36835 cbvmpo2 43557 cbvmpo1 43558 mpomptx2 46658 cbvmpox2 46659 |
Copyright terms: Public domain | W3C validator |