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

Definition df-mpt 4512
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from (in ) to (x)." The class expression is the value of the function at and normally contains the variable . An example is the square function for complex numbers, . Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Definition df-mpt
StepHypRef Expression
1 vx . . 3
2 cA . . 3
3 cB . . 3
41, 2, 3cmpt 4510 . 2
51cv 1394 . . . . 5
65, 2wcel 1818 . . . 4
7 vy . . . . . 6
87cv 1394 . . . . 5
98, 3wceq 1395 . . . 4
106, 9wa 369 . . 3
1110, 1, 7copab 4509 . 2
124, 11wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4528  nfmpt  4540  nfmpt1  4541  cbvmpt  4542  mptv  4544  csbmpt12  4786  fconstmpt  5048  rnmpt  5253  resmpt  5328  mptresid  5333  mptcnv  5413  mptpreima  5505  funmpt  5629  dfmpt3  5708  mptfng  5711  mptun  5717  dffn5  5918  fvmptg  5954  fndmin  5994  f1ompt  6053  fmptco  6064  fmptsng  6092  fmptsnd  6093  mpt2mptx  6393  f1ocnvd  6524  dftpos4  6993  mpt2curryd  7017  mapsncnv  7485  marypha2lem3  7917  cardf2  8345  aceq3lem  8522  compsscnv  8772  swrd0  12658  pjfval2  18740  2ndcdisj  19957  xkocnv  20315  clwwlknprop  24772  abrexexd  27407  f1o3d  27471  cbvmptf  27494  mptfnf  27499  feqmptdf  27501  fmptcof2  27502  mpt2mptxf  27518  f1od2  27547  qqhval2  27963  dfid4  29103  mptrel  29198  mpteq12d  29202  dfbigcup2  29549  mbfposadd  30062  fnopabco  30213  mptbi12f  30575  fgraphopab  31170  dfafn5a  32245  mpt2mptx2  32924
  Copyright terms: Public domain W3C validator