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

Definition df-mpt 4019
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 4017 . 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 4016 . 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  4036  nfmpt  4048  nfmpt1  4049  cbvmpt  4050  mptv  4052  fconstmpt  4685  rnmpt  4878  resmpt  4953  mptresid  4957  mptpreima  5118  funmpt  5194  dfmpt3  5269  mptfng  5272  mptun  5277  dffn5  5467  fvmptg  5499  fndmin  5531  f1ompt  5581  fmptco  5590  mpt2mptx  5837  f1ocnvd  5965  dftpos4  6152  mapsncnv  6747  marypha2lem3  7123  cardf2  7509  aceq3lem  7680  compsscnv  7930  fsumrev  12171  fsumshft  12172  pjfval2  16536  2ndcdisj  17109  pt1hmeo  17424  xkocnv  17432  mptcnv  22952  f1o3d  22963  mptrel  23458  mpteq12d  23462  dfbigcup2  23780  fnovpop  24369  dffn5a  24462  trnij  24947  fnopabco  25720  fgraphopab  26861
  Copyright terms: Public domain W3C validator