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 4729 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1482 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 1990 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1482 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1483 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 384 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 4712 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1483 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12f 4731 mpteq12d 4734 mpteq12df 4735 nfmpt 4746 nfmpt1 4747 cbvmptf 4748 cbvmpt 4749 mptv 4751 csbmpt12 5010 dfid4 5026 fconstmpt 5163 mptrel 5248 rnmpt 5371 resmpt 5449 mptresid 5456 mptcnv 5534 mptpreima 5628 funmpt 5926 dfmpt3 6014 mptfnf 6015 mptfng 6019 mptun 6025 dffn5 6241 feqmptdf 6251 fvmptg 6280 fvmptndm 6308 fndmin 6324 f1ompt 6382 fmptco 6396 fmptsng 6434 fmptsnd 6435 mpt2mptx 6751 f1ocnvd 6884 dftpos4 7371 mpt2curryd 7395 mapsncnv 7904 marypha2lem3 8343 cardf2 8769 aceq3lem 8943 compsscnv 9193 pjfval2 20053 2ndcdisj 21259 xkocnv 21617 abrexexd 29347 f1o3d 29431 fmptcof2 29457 mptssALT 29474 mpt2mptxf 29477 f1od2 29499 qqhval2 30026 dfbigcup2 32006 bj-0nelmpt 33069 bj-mpt2mptALT 33072 rnmptsn 33182 curf 33387 curunc 33391 phpreu 33393 poimirlem26 33435 mbfposadd 33457 fnopabco 33517 mptbi12f 33975 fgraphopab 37788 mptssid 39450 dfafn5a 41240 mpt2mptx2 42113 |
Copyright terms: Public domain | W3C validator |