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

Definition df-mpt 4228
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 4226 . 2  class  ( x  e.  A  |->  B )
51cv 1648 . . . . 5  class  x
65, 2wcel 1721 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1648 . . . . 5  class  y
98, 3wceq 1649 . . . 4  wff  y  =  B
106, 9wa 359 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4225 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1649 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  4245  nfmpt  4257  nfmpt1  4258  cbvmpt  4259  mptv  4261  fconstmpt  4880  rnmpt  5075  resmpt  5150  mptresid  5154  mptpreima  5322  funmpt  5448  dfmpt3  5526  mptfng  5529  mptun  5534  dffn5  5731  fvmptg  5763  fndmin  5796  f1ompt  5850  fmptco  5860  mpt2mptx  6123  f1ocnvd  6252  dftpos4  6457  mapsncnv  7019  marypha2lem3  7400  cardf2  7786  aceq3lem  7957  compsscnv  8207  fsumrev  12517  fsumshft  12518  pjfval2  16891  2ndcdisj  17472  pt1hmeo  17791  xkocnv  17799  abrexexd  23943  f1o3d  23994  mptcnv  23998  cbvmptf  24021  mptfnf  24026  feqmptdf  24028  fmptcof2  24029  qqhval2  24319  dfid4  25136  fprodshft  25253  fprodrev  25254  mptrel  25338  mpteq12d  25342  dfbigcup2  25653  fnopabco  26314  fgraphopab  27397  dfafn5a  27891
  Copyright terms: Public domain W3C validator