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

Definition df-mpt 4260
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 4258 . 2  class  ( x  e.  A  |->  B )
51cv 1651 . . . . 5  class  x
65, 2wcel 1725 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1651 . . . . 5  class  y
98, 3wceq 1652 . . . 4  wff  y  =  B
106, 9wa 359 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4257 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1652 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  4277  nfmpt  4289  nfmpt1  4290  cbvmpt  4291  mptv  4293  fconstmpt  4912  rnmpt  5107  resmpt  5182  mptresid  5186  mptpreima  5354  funmpt  5480  dfmpt3  5558  mptfng  5561  mptun  5566  dffn5  5763  fvmptg  5795  fndmin  5828  f1ompt  5882  fmptco  5892  mpt2mptx  6155  f1ocnvd  6284  dftpos4  6489  mapsncnv  7051  marypha2lem3  7433  cardf2  7819  aceq3lem  7990  compsscnv  8240  fsumrev  12550  fsumshft  12551  pjfval2  16924  2ndcdisj  17507  pt1hmeo  17826  xkocnv  17834  abrexexd  23978  f1o3d  24029  mptcnv  24033  cbvmptf  24056  mptfnf  24061  feqmptdf  24063  fmptcof2  24064  qqhval2  24354  dfid4  25171  fprodshft  25289  fprodrev  25290  mptrel  25379  mpteq12d  25383  dfbigcup2  25694  fnopabco  26361  fgraphopab  27444  dfafn5a  27938
  Copyright terms: Public domain W3C validator