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

Definition df-mpt 4053
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 4051 . 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 4050 . 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  4070  nfmpt  4082  nfmpt1  4083  cbvmpt  4084  mptv  4086  fconstmpt  4720  rnmpt  4913  resmpt  4988  mptresid  4992  mptpreima  5153  funmpt  5229  dfmpt3  5304  mptfng  5307  mptun  5312  dffn5  5502  fvmptg  5534  fndmin  5566  f1ompt  5616  fmptco  5625  mpt2mptx  5872  f1ocnvd  6000  dftpos4  6187  mapsncnv  6782  marypha2lem3  7158  cardf2  7544  aceq3lem  7715  compsscnv  7965  fsumrev  12207  fsumshft  12208  pjfval2  16572  2ndcdisj  17145  pt1hmeo  17460  xkocnv  17468  mptcnv  22988  f1o3d  22999  mptrel  23494  mpteq12d  23498  dfbigcup2  23816  fnovpop  24405  dffn5a  24498  trnij  24983  fnopabco  25756  fgraphopab  26897
  Copyright terms: Public domain W3C validator