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

Definition df-mpt 3878
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 3876 . 2 class (𝑥𝐴𝐵)
51cv 1286 . . . . 5 class 𝑥
65, 2wcel 1436 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1286 . . . . 5 class 𝑦
98, 3wceq 1287 . . . 4 wff 𝑦 = 𝐵
106, 9wa 102 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 3875 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1287 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3895  nfmpt  3907  nfmpt1  3908  cbvmptf  3909  cbvmpt  3910  mptv  3912  fconstmpt  4455  rnmpt  4653  resmpt  4729  mptresid  4735  mptpreima  4892  funmpt  5019  dfmpt3  5103  mptfng  5106  mptun  5111  dffn5im  5315  fvmptss2  5344  fvmptg  5345  fndmin  5371  f1ompt  5415  fmptco  5429  mpt2mptx  5698  f1ocnvd  5805  f1od2  5959  dftpos4  5984  mapsncnv  6406
  Copyright terms: Public domain W3C validator