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

Definition df-mpt 4095
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 4093 . 2  class  ( x  e.  A  |->  B )
51cv 1631 . . . . 5  class  x
65, 2wcel 1696 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1631 . . . . 5  class  y
98, 3wceq 1632 . . . 4  wff  y  =  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4092 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1632 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  4112  nfmpt  4124  nfmpt1  4125  cbvmpt  4126  mptv  4128  fconstmpt  4748  rnmpt  4941  resmpt  5016  mptresid  5020  mptpreima  5182  funmpt  5306  dfmpt3  5382  mptfng  5385  mptun  5390  dffn5  5584  fvmptg  5616  fndmin  5648  f1ompt  5698  fmptco  5707  mpt2mptx  5954  f1ocnvd  6082  dftpos4  6269  mapsncnv  6830  marypha2lem3  7206  cardf2  7592  aceq3lem  7763  compsscnv  8013  fsumrev  12257  fsumshft  12258  pjfval2  16625  2ndcdisj  17198  pt1hmeo  17513  xkocnv  17521  mptcnv  23043  f1o3d  23053  abrexexd  23207  cbvmptf  23235  mptfnf  23241  feqmptdf  23243  fmptcof2  23244  mptrel  24195  mpteq12d  24199  dfbigcup2  24510  fnovpop  25141  dffn5a  25233  trnij  25718  fnopabco  26491  fgraphopab  27632  dfafn5a  28128  eupatrl  28385
  Copyright terms: Public domain W3C validator