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

Definition df-mpt 3876
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 3874 . 2  class  ( x  e.  A  |->  B )
51cv 1286 . . . . 5  class  x
65, 2wcel 1436 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1286 . . . . 5  class  y
98, 3wceq 1287 . . . 4  wff  y  =  B
106, 9wa 102 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3873 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1287 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  3893  nfmpt  3905  nfmpt1  3906  cbvmptf  3907  cbvmpt  3908  mptv  3910  fconstmpt  4453  rnmpt  4651  resmpt  4727  mptresid  4733  mptpreima  4890  funmpt  5017  dfmpt3  5101  mptfng  5104  mptun  5109  dffn5im  5313  fvmptss2  5342  fvmptg  5343  fndmin  5369  f1ompt  5413  fmptco  5427  mpt2mptx  5696  f1ocnvd  5803  f1od2  5957  dftpos4  5982  mapsncnv  6404
  Copyright terms: Public domain W3C validator