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

Definition df-mpt 4000
 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
2 cA . . 3
3 cB . . 3
41, 2, 3cmpt 3998 . 2
51cv 1331 . . . . 5
65, 2wcel 1481 . . . 4
7 vy . . . . . 6
87cv 1331 . . . . 5
98, 3wceq 1332 . . . 4
106, 9wa 103 . . 3
1110, 1, 7copab 3997 . 2
124, 11wceq 1332 1
 Colors of variables: wff set class This definition is referenced by:  mpteq12f  4017  nfmpt  4029  nfmpt1  4030  cbvmptf  4031  cbvmpt  4032  mptv  4034  fconstmpt  4597  mptrel  4678  rnmpt  4798  resmpt  4878  mptresid  4884  mptcnv  4952  mptpreima  5043  funmpt  5172  dfmpt3  5256  mptfng  5259  mptun  5265  dffn5im  5478  fvmptss2  5507  fvmptg  5508  fndmin  5538  f1ompt  5582  fmptco  5597  mpomptx  5873  f1ocnvd  5983  f1od2  6143  dftpos4  6171  mapsncnv  6600
 Copyright terms: Public domain W3C validator