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

Definition df-mpt 4080
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 4078 . 2  class  ( x  e.  A  |->  B )
51cv 1622 . . . . 5  class  x
65, 2wcel 1685 . . . 4  wff  x  e.  A
7 vy . . . . . 6  set  y
87cv 1622 . . . . 5  class  y
98, 3wceq 1623 . . . 4  wff  y  =  B
106, 9wa 358 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 4077 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1623 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  4097  nfmpt  4109  nfmpt1  4110  cbvmpt  4111  mptv  4113  fconstmpt  4731  rnmpt  4924  resmpt  4999  mptresid  5003  mptpreima  5164  funmpt  5256  dfmpt3  5332  mptfng  5335  mptun  5340  dffn5  5530  fvmptg  5562  fndmin  5594  f1ompt  5644  fmptco  5653  mpt2mptx  5900  f1ocnvd  6028  dftpos4  6215  mapsncnv  6810  marypha2lem3  7186  cardf2  7572  aceq3lem  7743  compsscnv  7993  fsumrev  12237  fsumshft  12238  pjfval2  16605  2ndcdisj  17178  pt1hmeo  17493  xkocnv  17501  mptcnv  23023  f1o3d  23033  mptrel  23528  mpteq12d  23532  dfbigcup2  23850  fnovpop  24448  dffn5a  24541  trnij  25026  fnopabco  25799  fgraphopab  26940  dfafn5a  27413
  Copyright terms: Public domain W3C validator