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

Definition df-mpt 4469
 Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from (in ) to B(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 4467 . 2
51cv 1369 . . . . 5
65, 2wcel 1758 . . . 4
7 vy . . . . . 6
87cv 1369 . . . . 5
98, 3wceq 1370 . . . 4
106, 9wa 369 . . 3
1110, 1, 7copab 4466 . 2
124, 11wceq 1370 1
 Colors of variables: wff setvar class This definition is referenced by:  mpteq12f  4485  nfmpt  4497  nfmpt1  4498  cbvmpt  4499  mptv  4501  csbmpt12  4739  fconstmpt  4999  rnmpt  5202  resmpt  5274  mptresid  5279  mptcnv  5358  mptpreima  5450  funmpt  5573  dfmpt3  5652  mptfng  5655  mptun  5661  dffn5  5860  fvmptg  5895  fndmin  5933  f1ompt  5988  fmptco  5999  fmptsng  6024  fmptsnd  6025  mpt2mptx  6314  f1ocnvd  6442  dftpos4  6898  mpt2curryd  6922  mapsncnv  7393  marypha2lem3  7823  cardf2  8250  aceq3lem  8427  compsscnv  8677  swrd0  12485  fsumrev  13404  pjfval2  18327  2ndcdisj  19459  pt1hmeo  19778  xkocnv  19786  abrexexd  26359  f1o3d  26416  cbvmptf  26438  mptfnf  26443  feqmptdf  26445  fmptcof2  26446  mpt2mptxf  26462  f1od2  26491  qqhval2  26868  dfid4  27838  fprodshft  27943  fprodrev  27944  mptrel  28035  mpteq12d  28039  dfbigcup2  28386  mbfposadd  28899  fnopabco  29076  mptbi12f  29439  fgraphopab  30038  dfafn5a  30943  clwwlknprop  31312  mpt2mptx2  31599
 Copyright terms: Public domain W3C validator