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

Definition df-mpt 4236
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 4234 . 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 4233 . 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  4253  nfmpt  4265  nfmpt1  4266  cbvmpt  4267  mptv  4269  fconstmpt  4888  rnmpt  5083  resmpt  5158  mptresid  5162  mptpreima  5330  funmpt  5456  dfmpt3  5534  mptfng  5537  mptun  5542  dffn5  5739  fvmptg  5771  fndmin  5804  f1ompt  5858  fmptco  5868  mpt2mptx  6131  f1ocnvd  6260  dftpos4  6465  mapsncnv  7027  marypha2lem3  7408  cardf2  7794  aceq3lem  7965  compsscnv  8215  fsumrev  12525  fsumshft  12526  pjfval2  16899  2ndcdisj  17480  pt1hmeo  17799  xkocnv  17807  abrexexd  23951  f1o3d  24002  mptcnv  24006  cbvmptf  24029  mptfnf  24034  feqmptdf  24036  fmptcof2  24037  qqhval2  24327  dfid4  25144  fprodshft  25261  fprodrev  25262  mptrel  25346  mpteq12d  25350  dfbigcup2  25661  fnopabco  26322  fgraphopab  27405  dfafn5a  27899
  Copyright terms: Public domain W3C validator