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

Definition df-mpt 3820
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 3818 . 2  class  ( x  e.  A  |->  B )
51cv 1242 . . . . 5  class  x
65, 2wcel 1393 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1242 . . . . 5  class  y
98, 3wceq 1243 . . . 4  wff  y  =  B
106, 9wa 97 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3817 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1243 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  3837  nfmpt  3849  nfmpt1  3850  cbvmpt  3851  mptv  3853  fconstmpt  4387  rnmpt  4582  resmpt  4656  mptresid  4660  mptpreima  4814  funmpt  4938  dfmpt3  5021  mptfng  5024  mptun  5029  dffn5im  5219  fvmptss2  5247  fvmptg  5248  fndmin  5274  f1ompt  5320  fmptco  5330  mpt2mptx  5595  f1ocnvd  5702  dftpos4  5878
  Copyright terms: Public domain W3C validator