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

Definition df-mpt 4352
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 4350 . 2
51cv 1368 . . . . 5
65, 2wcel 1756 . . . 4
7 vy . . . . . 6
87cv 1368 . . . . 5
98, 3wceq 1369 . . . 4
106, 9wa 369 . . 3
1110, 1, 7copab 4349 . 2
124, 11wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4368  nfmpt  4380  nfmpt1  4381  cbvmpt  4382  mptv  4384  csbmpt12  4622  fconstmpt  4882  rnmpt  5085  resmpt  5156  mptresid  5160  mptcnv  5239  mptpreima  5331  funmpt  5454  dfmpt3  5533  mptfng  5536  mptun  5541  dffn5  5737  fvmptg  5772  fndmin  5810  f1ompt  5865  fmptco  5876  fmptsng  5900  mpt2mptx  6181  f1ocnvd  6309  dftpos4  6764  mpt2curryd  6788  mapsncnv  7259  marypha2lem3  7687  cardf2  8113  aceq3lem  8290  compsscnv  8540  swrd0  12327  fsumrev  13246  pjfval2  18134  2ndcdisj  19060  pt1hmeo  19379  xkocnv  19387  abrexexd  25890  f1o3d  25948  cbvmptf  25971  mptfnf  25976  feqmptdf  25978  fmptcof2  25979  mpt2mptxf  25995  f1od2  26024  qqhval2  26411  dfid4  27382  fprodshft  27487  fprodrev  27488  mptrel  27579  mpteq12d  27583  dfbigcup2  27930  mbfposadd  28439  fnopabco  28616  mptbi12f  28979  fgraphopab  29578  dfafn5a  30066  clwwlknprop  30435  fmptsnd  30722  mpt2mptx2  30724
  Copyright terms: Public domain W3C validator