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 which maps 𝑥 (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 5138 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1527 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1527 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1528 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 5120 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1528 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12df 5140 mpteq12f 5141 nfmpt 5155 nfmpt1 5156 cbvmptf 5157 cbvmptfg 5158 mptv 5163 csbmpt12 5436 dfid4 5455 fconstmpt 5608 mptrel 5691 rnmpt 5821 resmpt 5899 mptresid 5912 mptresidOLD 5914 mptcnv 5992 mptpreima 6086 funmpt 6387 dfmpt3 6476 mptfnf 6477 mptfng 6481 mptun 6488 dffn5 6718 feqmptdf 6729 fvmptg 6760 fvmptndm 6791 fndmin 6808 f1ompt 6868 fmptco 6884 fmptsng 6923 fmptsnd 6924 mpomptx 7254 f1ocnvd 7385 dftpos4 7902 mpocurryd 7926 mapsncnv 8446 marypha2lem3 8890 cardf2 9361 aceq3lem 9535 compsscnv 9782 pjfval2 20783 2ndcdisj 21994 xkocnv 22352 abrexexd 30197 f1o3d 30301 fmptcof2 30331 mptssALT 30349 mpomptxf 30354 f1od2 30384 qqhval2 31123 dfbigcup2 33258 bj-0nelmpt 34301 bj-mpomptALT 34304 rnmptsn 34499 curf 34752 curunc 34756 phpreu 34758 poimirlem26 34800 mbfposadd 34821 fnopabco 34881 mptbi12f 35327 fgraphopab 39690 mptssid 41391 dfafn5a 43240 mpomptx2 44281 |
Copyright terms: Public domain | W3C validator |