New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-mpt GIF 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 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 SF, 5-Jan-2015.)
Assertion
Ref Expression
df-mpt (x A B) = {x, y (x 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 5651 . 2 class (x A B)
51cv 1641 . . . . 5 class x
65, 2wcel 1710 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1641 . . . . 5 class y
98, 3wceq 1642 . . . 4 wff y = B
106, 9wa 358 . . 3 wff (x A y = B)
1110, 1, 7copab 4622 . 2 class {x, y (x A y = B)}
124, 11wceq 1642 1 wff (x A B) = {x, y (x A y = B)}
 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  6331
 Copyright terms: Public domain W3C validator