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

Definition df-mpt 3783
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 3781 . 2 class (x AB)
51cv 1222 . . . . 5 class x
65, 2wcel 1366 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1222 . . . . 5 class y
98, 3wceq 1223 . . . 4 wff y = B
106, 9wa 97 . . 3 wff (x A y = B)
1110, 1, 7copab 3780 . 2 class {⟨x, y⟩ ∣ (x A y = B)}
124, 11wceq 1223 1 wff (x AB) = {⟨x, y⟩ ∣ (x A y = B)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3800  nfmpt  3812  nfmpt1  3813  cbvmpt  3814  mptv  3816  fconstmpt  4302  rnmpt  4497  resmpt  4571  mptresid  4575  mptpreima  4729  funmpt  4852  dfmpt3  4935  mptfng  4938  mptun  4943  dffn5im  5132  fvmptss2  5160  fvmptg  5161  fndmin  5187  f1ompt  5233  fmptco  5243  mpt2mptx  5506  f1ocnvd  5613  dftpos4  5788
  Copyright terms: Public domain W3C validator