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

Definition df-mpt 3961
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 3959 . 2 class (𝑥𝐴𝐵)
51cv 1315 . . . . 5 class 𝑥
65, 2wcel 1465 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1315 . . . . 5 class 𝑦
98, 3wceq 1316 . . . 4 wff 𝑦 = 𝐵
106, 9wa 103 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 3958 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1316 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3978  nfmpt  3990  nfmpt1  3991  cbvmptf  3992  cbvmpt  3993  mptv  3995  fconstmpt  4556  mptrel  4637  rnmpt  4757  resmpt  4837  mptresid  4843  mptcnv  4911  mptpreima  5002  funmpt  5131  dfmpt3  5215  mptfng  5218  mptun  5224  dffn5im  5435  fvmptss2  5464  fvmptg  5465  fndmin  5495  f1ompt  5539  fmptco  5554  mpomptx  5830  f1ocnvd  5940  f1od2  6100  dftpos4  6128  mapsncnv  6557
  Copyright terms: Public domain W3C validator