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

Definition df-mpt 4268
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 4266 . 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 4265 . 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  4285  nfmpt  4297  nfmpt1  4298  cbvmpt  4299  mptv  4301  fconstmpt  4921  rnmpt  5116  resmpt  5191  mptresid  5195  mptpreima  5363  funmpt  5489  dfmpt3  5567  mptfng  5570  mptun  5575  dffn5  5772  fvmptg  5804  fndmin  5837  f1ompt  5891  fmptco  5901  mpt2mptx  6164  f1ocnvd  6293  dftpos4  6498  mapsncnv  7060  marypha2lem3  7442  cardf2  7830  aceq3lem  8001  compsscnv  8251  fsumrev  12562  fsumshft  12563  pjfval2  16936  2ndcdisj  17519  pt1hmeo  17838  xkocnv  17846  abrexexd  23990  f1o3d  24041  mptcnv  24045  cbvmptf  24068  mptfnf  24073  feqmptdf  24075  fmptcof2  24076  qqhval2  24366  dfid4  25183  fprodshft  25300  fprodrev  25301  mptrel  25392  mpteq12d  25396  dfbigcup2  25744  fnopabco  26424  fgraphopab  27506  dfafn5a  28000
  Copyright terms: Public domain W3C validator