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

Definition df-mpt 3976
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 3974 . 2  class  ( x  e.  A  |->  B )
51cv 1618 . . . . 5  class  x
65, 2wcel 1621 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1618 . . . . 5  class  y
98, 3wceq 1619 . . . 4  wff  y  =  B
106, 9wa 360 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3973 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1619 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  3993  nfmpt  4005  nfmpt1  4006  cbvmpt  4007  mptv  4009  fconstmpt  4639  rnmpt  4832  resmpt  4907  mptresid  4911  mptpreima  5072  funmpt  5148  dfmpt3  5223  mptfng  5226  mptun  5231  dffn5  5420  fvmptg  5452  fndmin  5484  f1ompt  5534  fmptco  5543  mpt2mptx  5790  f1ocnvd  5918  dftpos4  6105  mapsncnv  6700  marypha2lem3  7074  cardf2  7460  aceq3lem  7631  compsscnv  7881  fsumrev  12118  fsumshft  12119  pjfval2  16441  2ndcdisj  17014  pt1hmeo  17329  xkocnv  17337  mptrel  23292  mpteq12d  23296  dfbigcup2  23614  fnovpop  24203  dffn5a  24296  trnij  24781  fnopabco  25554  fgraphopab  26695
  Copyright terms: Public domain W3C validator