Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpt Structured version   Visualization version   GIF version

Definition df-mpt 4645
 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.)
Assertion
Ref Expression
df-mpt (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-mpt
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cmpt 4643 . 2 class (𝑥𝐴𝐵)
51cv 1474 . . . . 5 class 𝑥
65, 2wcel 1977 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1474 . . . . 5 class 𝑦
98, 3wceq 1475 . . . 4 wff 𝑦 = 𝐵
106, 9wa 383 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4642 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 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