![]() |
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 4873 | . 2 class (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 1 | cv 1623 | . . . . 5 class 𝑥 |
6 | 5, 2 | wcel 2131 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1623 | . . . . 5 class 𝑦 |
9 | 8, 3 | wceq 1624 | . . . 4 wff 𝑦 = 𝐵 |
10 | 6, 9 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
11 | 10, 1, 7 | copab 4856 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
12 | 4, 11 | wceq 1624 | 1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: mpteq12f 4875 mpteq12d 4878 mpteq12df 4879 nfmpt 4890 nfmpt1 4891 cbvmptf 4892 cbvmpt 4893 mptv 4895 csbmpt12 5152 dfid4 5168 fconstmpt 5312 mptrel 5396 rnmpt 5518 resmpt 5599 mptresid 5606 mptcnv 5684 mptpreima 5781 funmpt 6079 dfmpt3 6167 mptfnf 6168 mptfng 6172 mptun 6178 dffn5 6395 feqmptdf 6405 fvmptg 6434 fvmptndm 6462 fndmin 6479 f1ompt 6537 fmptco 6551 fmptsng 6590 fmptsnd 6591 mpt2mptx 6908 f1ocnvd 7041 dftpos4 7532 mpt2curryd 7556 mapsncnv 8062 marypha2lem3 8500 cardf2 8951 aceq3lem 9125 compsscnv 9377 pjfval2 20247 2ndcdisj 21453 xkocnv 21811 abrexexd 29646 f1o3d 29732 fmptcof2 29758 mptssALT 29775 mpt2mptxf 29778 f1od2 29800 qqhval2 30327 dfbigcup2 32304 bj-0nelmpt 33367 bj-mpt2mptALT 33370 rnmptsn 33485 curf 33692 curunc 33696 phpreu 33698 poimirlem26 33740 mbfposadd 33762 fnopabco 33822 mptbi12f 34280 fgraphopab 38282 mptssid 39941 dfafn5a 41738 mpt2mptx2 42615 |
Copyright terms: Public domain | W3C validator |