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

Definition df-mpt 4079
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 4077 . 2  class  ( x  e.  A  |->  B )
51cv 1622 . . . . 5  class  x
65, 2wcel 1684 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1622 . . . . 5  class  y
98, 3wceq 1623 . . . 4  wff  y  =  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4076 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1623 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  4096  nfmpt  4108  nfmpt1  4109  cbvmpt  4110  mptv  4112  fconstmpt  4732  rnmpt  4925  resmpt  5000  mptresid  5004  mptpreima  5166  funmpt  5290  dfmpt3  5366  mptfng  5369  mptun  5374  dffn5  5568  fvmptg  5600  fndmin  5632  f1ompt  5682  fmptco  5691  mpt2mptx  5938  f1ocnvd  6066  dftpos4  6253  mapsncnv  6814  marypha2lem3  7190  cardf2  7576  aceq3lem  7747  compsscnv  7997  fsumrev  12241  fsumshft  12242  pjfval2  16609  2ndcdisj  17182  pt1hmeo  17497  xkocnv  17505  mptcnv  23027  f1o3d  23037  abrexexd  23192  cbvmptf  23220  mptfnf  23226  feqmptdf  23228  fmptcof2  23229  mptrel  24124  mpteq12d  24128  dfbigcup2  24439  fnovpop  25038  dffn5a  25130  trnij  25615  fnopabco  26388  fgraphopab  27529  dfafn5a  28022
  Copyright terms: Public domain W3C validator