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

Definition df-mpt 3931
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 3929 . 2  class  ( x  e.  A  |->  B )
51cv 1298 . . . . 5  class  x
65, 2wcel 1448 . . . 4  wff  x  e.  A
7 vy . . . . . 6  setvar  y
87cv 1298 . . . . 5  class  y
98, 3wceq 1299 . . . 4  wff  y  =  B
106, 9wa 103 . . 3  wff  ( x  e.  A  /\  y  =  B )
1110, 1, 7copab 3928 . 2  class  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
124, 11wceq 1299 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  3948  nfmpt  3960  nfmpt1  3961  cbvmptf  3962  cbvmpt  3963  mptv  3965  fconstmpt  4524  mptrel  4605  rnmpt  4725  resmpt  4803  mptresid  4809  mptcnv  4877  mptpreima  4968  funmpt  5097  dfmpt3  5181  mptfng  5184  mptun  5190  dffn5im  5399  fvmptss2  5428  fvmptg  5429  fndmin  5459  f1ompt  5503  fmptco  5518  mpomptx  5794  f1ocnvd  5904  f1od2  6062  dftpos4  6090  mapsncnv  6519
  Copyright terms: Public domain W3C validator