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

Definition df-mpt 3790
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 NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt (x AB) = {⟨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 3788 . 2 class (x AB)
51cv 1225 . . . . 5 class x
65, 2wcel 1370 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1225 . . . . 5 class y
98, 3wceq 1226 . . . 4 wff y = B
106, 9wa 97 . . 3 wff (x A y = B)
1110, 1, 7copab 3787 . 2 class {⟨x, y⟩ ∣ (x A y = B)}
124, 11wceq 1226 1 wff (x AB) = {⟨x, y⟩ ∣ (x A y = B)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3807  nfmpt  3819  nfmpt1  3820  cbvmpt  3821  mptv  3823  fconstmpt  4310  rnmpt  4505  resmpt  4579  mptresid  4583  mptpreima  4737  funmpt  4860  dfmpt3  4943  mptfng  4946  mptun  4951  dffn5im  5140  fvmptss2  5168  fvmptg  5169  fndmin  5195  f1ompt  5241  fmptco  5251  mpt2mptx  5514  f1ocnvd  5621  dftpos4  5796
  Copyright terms: Public domain W3C validator