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

Definition df-mpt 4081
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 NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-mpt
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cmpt 4079 . 2 class (𝑥𝐴𝐵)
51cv 1363 . . . . 5 class 𝑥
65, 2wcel 2160 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1363 . . . . 5 class 𝑦
98, 3wceq 1364 . . . 4 wff 𝑦 = 𝐵
106, 9wa 104 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4078 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1364 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  4098  nfmpt  4110  nfmpt1  4111  cbvmptf  4112  cbvmpt  4113  mptv  4115  fconstmpt  4691  mptrel  4773  rnmpt  4893  resmpt  4973  mptresid  4979  mptcnv  5049  mptpreima  5140  funmpt  5273  dfmpt3  5357  mptfng  5360  mptun  5366  dffn5im  5581  fvmptss2  5611  fvmptg  5612  fndmin  5643  f1ompt  5687  fmptco  5702  mpomptx  5986  f1ocnvd  6095  f1od2  6259  dftpos4  6287  mapsncnv  6720
  Copyright terms: Public domain W3C validator