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

Definition df-mpt 3847
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 3845 . 2  class  ( x  e.  A  |->  B )
51cv 1258 . . . . 5  class  x
65, 2wcel 1409 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1258 . . . . 5  class  y
98, 3wceq 1259 . . . 4  wff  y  =  B
106, 9wa 101 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3844 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1259 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  3864  nfmpt  3876  nfmpt1  3877  cbvmpt  3878  mptv  3880  fconstmpt  4414  rnmpt  4609  resmpt  4683  mptresid  4687  mptpreima  4841  funmpt  4965  dfmpt3  5048  mptfng  5051  mptun  5056  dffn5im  5246  fvmptss2  5274  fvmptg  5275  fndmin  5301  f1ompt  5347  fmptco  5357  mpt2mptx  5622  f1ocnvd  5729  f1od2  5883  dftpos4  5908
  Copyright terms: Public domain W3C validator