Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-mpt | Structured version Visualization version GIF version |
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (in 𝐴) to 𝐵(𝑥)." The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. An example is the square function for complex numbers, (𝑥 ∈ ℂ ↦ (𝑥↑2)). Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpt | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar 𝑥 | |
2 | cA | . . 3 class 𝐴 | |
3 | cB | . . 3 class 𝐵 | |
4 | 1, 2, 3 | cmpt 4643 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1474 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1475 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 4642 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1475 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12f 4661 nfmpt 4674 nfmpt1 4675 cbvmptf 4676 cbvmpt 4677 mptv 4679 csbmpt12 4934 dfid4 4955 fconstmpt 5085 mptrel 5170 rnmpt 5292 resmpt 5369 mptresid 5375 mptcnv 5453 mptpreima 5545 funmpt 5840 dfmpt3 5927 mptfnf 5928 mptfng 5932 mptun 5938 dffn5 6151 feqmptdf 6161 fvmptg 6189 fvmptndm 6216 fndmin 6232 f1ompt 6290 fmptco 6303 fmptsng 6339 fmptsnd 6340 mpt2mptx 6649 f1ocnvd 6782 dftpos4 7258 mpt2curryd 7282 mapsncnv 7790 marypha2lem3 8226 cardf2 8652 aceq3lem 8826 compsscnv 9076 pjfval2 19872 2ndcdisj 21069 xkocnv 21427 clwwlknprop 26300 abrexexd 28731 f1o3d 28813 mpteq12df 28837 fmptcof2 28839 mptssALT 28857 mpt2mptxf 28860 f1od2 28887 qqhval2 29354 mpteq12d 30915 dfbigcup2 31176 bj-0nelmpt 32250 bj-mpt2mptALT 32253 rnmptsn 32358 curf 32557 curunc 32561 phpreu 32563 poimirlem26 32605 mbfposadd 32627 fnopabco 32687 mptbi12f 33145 fgraphopab 36807 dfafn5a 39889 mpt2mptx2 41906 |
Copyright terms: Public domain | W3C validator |