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

Definition df-mpt 4081
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from  x (in 
A) to  B ( x )." The class expression  B is the value of the function at  x and normally contains the variable  x. An example is the square function for complex numbers,  ( x  e.  CC  |->  ( x ^ 2 ) ). Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
Distinct variable groups:    x, y    y, A    y, B
Allowed substitution hints:    A( x)    B( x)

Detailed syntax breakdown of Definition df-mpt
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3cmpt 4079 . 2  class  ( x  e.  A  |->  B )
51cv 1624 . . . . 5  class  x
65, 2wcel 1686 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1624 . . . . 5  class  y
98, 3wceq 1625 . . . 4  wff  y  =  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4078 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1625 1  wff  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  4098  nfmpt  4110  nfmpt1  4111  cbvmpt  4112  mptv  4114  fconstmpt  4734  rnmpt  4927  resmpt  5002  mptresid  5006  mptpreima  5168  funmpt  5292  dfmpt3  5368  mptfng  5371  mptun  5376  dffn5  5570  fvmptg  5602  fndmin  5634  f1ompt  5684  fmptco  5693  mpt2mptx  5940  f1ocnvd  6068  dftpos4  6255  mapsncnv  6816  marypha2lem3  7192  cardf2  7578  aceq3lem  7749  compsscnv  7999  fsumrev  12243  fsumshft  12244  pjfval2  16611  2ndcdisj  17184  pt1hmeo  17499  xkocnv  17507  mptcnv  23029  f1o3d  23039  abrexexd  23194  cbvmptf  23222  mptfnf  23228  feqmptdf  23230  fmptcof2  23231  mptrel  24126  mpteq12d  24130  dfbigcup2  24441  fnovpop  25049  dffn5a  25141  trnij  25626  fnopabco  26399  fgraphopab  27540  dfafn5a  28033
  Copyright terms: Public domain W3C validator