ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mpt Unicode version

Definition df-mpt 3867
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. 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  setvar  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3cmpt 3865 . 2  class  ( x  e.  A  |->  B )
51cv 1284 . . . . 5  class  x
65, 2wcel 1434 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1284 . . . . 5  class  y
98, 3wceq 1285 . . . 4  wff  y  =  B
106, 9wa 102 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3864 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1285 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  3884  nfmpt  3896  nfmpt1  3897  cbvmpt  3898  mptv  3900  fconstmpt  4443  rnmpt  4641  resmpt  4717  mptresid  4721  mptpreima  4878  funmpt  5005  dfmpt3  5089  mptfng  5092  mptun  5097  dffn5im  5295  fvmptss2  5324  fvmptg  5325  fndmin  5351  f1ompt  5395  fmptco  5406  mpt2mptx  5674  f1ocnvd  5781  f1od2  5935  dftpos4  5960  mapsncnv  6382
  Copyright terms: Public domain W3C validator