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

Definition df-mpt 4202
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 4200 . 2  class  ( x  e.  A  |->  B )
51cv 1648 . . . . 5  class  x
65, 2wcel 1717 . . . 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 4199 . 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  4219  nfmpt  4231  nfmpt1  4232  cbvmpt  4233  mptv  4235  fconstmpt  4854  rnmpt  5049  resmpt  5124  mptresid  5128  mptpreima  5296  funmpt  5422  dfmpt3  5500  mptfng  5503  mptun  5508  dffn5  5704  fvmptg  5736  fndmin  5769  f1ompt  5823  fmptco  5833  mpt2mptx  6096  f1ocnvd  6225  dftpos4  6427  mapsncnv  6989  marypha2lem3  7370  cardf2  7756  aceq3lem  7927  compsscnv  8177  fsumrev  12482  fsumshft  12483  pjfval2  16852  2ndcdisj  17433  pt1hmeo  17752  xkocnv  17760  abrexexd  23827  f1o3d  23877  mptcnv  23881  cbvmptf  23903  mptfnf  23908  feqmptdf  23910  fmptcof2  23911  qqhval2  24158  dfid4  24955  fprodshft  25072  fprodrev  25073  mptrel  25141  mpteq12d  25145  dfbigcup2  25456  fnopabco  26108  fgraphopab  27191  dfafn5a  27686
  Copyright terms: Public domain W3C validator