NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-mpt Unicode version

Definition df-mpt 5653
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 SF, 5-Jan-2015.)
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 5652 . 2
51cv 1641 . . . . 5
65, 2wcel 1710 . . . 4
7 vy . . . . . 6
87cv 1641 . . . . 5
98, 3wceq 1642 . . . 4
106, 9wa 358 . . 3
1110, 1, 7copab 4623 . 2
124, 11wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  5656  nfmpt  5672  nfmpt1  5673  cbvmpt  5677  fconstmpt  5682  mptpreima  5683  dmmpt  5684  dmmptss  5686  rnmpt  5687  funmpt  5688  mptfng  5689  resmpt  5697  fvmptg  5699  dffn5v  5707  mpt2mptx  5709  mptv  5719  mptresid  5721  f1od  5727  releqmpt  5809  enmap2lem1  6064  enmap1lem1  6070  scancan  6332
  Copyright terms: Public domain W3C validator