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

Definition df-mpt 5652
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 5651 . 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 4622 . 2
124, 11wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  5655  nfmpt  5671  nfmpt1  5672  cbvmpt  5676  fconstmpt  5681  mptpreima  5682  dmmpt  5683  dmmptss  5685  rnmpt  5686  funmpt  5687  mptfng  5688  resmpt  5696  fvmptg  5698  dffn5v  5706  mpt2mptx  5708  mptv  5718  mptresid  5720  f1od  5726  releqmpt  5808  enmap2lem1  6063  enmap1lem1  6069  scancan  6329
  Copyright terms: Public domain W3C validator