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

Definition df-mpt 3848
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 3846 . 2 class (𝑥𝐴𝐵)
51cv 1258 . . . . 5 class 𝑥
65, 2wcel 1409 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1258 . . . . 5 class 𝑦
98, 3wceq 1259 . . . 4 wff 𝑦 = 𝐵
106, 9wa 101 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 3845 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1259 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  3865  nfmpt  3877  nfmpt1  3878  cbvmpt  3879  mptv  3881  fconstmpt  4415  rnmpt  4610  resmpt  4684  mptresid  4688  mptpreima  4842  funmpt  4966  dfmpt3  5049  mptfng  5052  mptun  5057  dffn5im  5247  fvmptss2  5275  fvmptg  5276  fndmin  5302  f1ompt  5348  fmptco  5358  mpt2mptx  5623  f1ocnvd  5730  f1od2  5884  dftpos4  5909
  Copyright terms: Public domain W3C validator