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

Definition df-mpt 3811
Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from (in ) to ." The class expression is the value of the function at and normally contains the variable . Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt  |->  { <. ,  >.  |  }
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-mpt
StepHypRef Expression
1 vx . . 3  setvar
2 cA . . 3
3 cB . . 3
41, 2, 3cmpt 3809 . 2  |->
51cv 1241 . . . . 5
65, 2wcel 1390 . . . 4
7 vy . . . . . 6  setvar
87cv 1241 . . . . 5
98, 3wceq 1242 . . . 4
106, 9wa 97 . . 3
1110, 1, 7copab 3808 . 2  { <. ,  >.  |  }
124, 11wceq 1242 1  |->  { <. ,  >.  |  }
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3828  nfmpt  3840  nfmpt1  3841  cbvmpt  3842  mptv  3844  fconstmpt  4330  rnmpt  4525  resmpt  4599  mptresid  4603  mptpreima  4757  funmpt  4881  dfmpt3  4964  mptfng  4967  mptun  4972  dffn5im  5162  fvmptss2  5190  fvmptg  5191  fndmin  5217  f1ompt  5263  fmptco  5273  mpt2mptx  5537  f1ocnvd  5644  dftpos4  5819
  Copyright terms: Public domain W3C validator