![]() |
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 4762 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1522 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 2030 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1522 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1523 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 4745 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1523 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12f 4764 mpteq12d 4767 mpteq12df 4768 nfmpt 4779 nfmpt1 4780 cbvmptf 4781 cbvmpt 4782 mptv 4784 csbmpt12 5039 dfid4 5055 fconstmpt 5197 mptrel 5281 rnmpt 5403 resmpt 5484 mptresid 5491 mptcnv 5569 mptpreima 5666 funmpt 5964 dfmpt3 6052 mptfnf 6053 mptfng 6057 mptun 6063 dffn5 6280 feqmptdf 6290 fvmptg 6319 fvmptndm 6347 fndmin 6364 f1ompt 6422 fmptco 6436 fmptsng 6475 fmptsnd 6476 mpt2mptx 6793 f1ocnvd 6926 dftpos4 7416 mpt2curryd 7440 mapsncnv 7946 marypha2lem3 8384 cardf2 8807 aceq3lem 8981 compsscnv 9231 pjfval2 20101 2ndcdisj 21307 xkocnv 21665 abrexexd 29473 f1o3d 29559 fmptcof2 29585 mptssALT 29602 mpt2mptxf 29605 f1od2 29627 qqhval2 30154 dfbigcup2 32131 bj-0nelmpt 33194 bj-mpt2mptALT 33197 rnmptsn 33312 curf 33517 curunc 33521 phpreu 33523 poimirlem26 33565 mbfposadd 33587 fnopabco 33647 mptbi12f 34105 fgraphopab 38105 mptssid 39764 dfafn5a 41561 mpt2mptx2 42438 |
Copyright terms: Public domain | W3C validator |