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

Definition df-mpt 3991
 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 3989 . 2 class (𝑥𝐴𝐵)
51cv 1330 . . . . 5 class 𝑥
65, 2wcel 1480 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1330 . . . . 5 class 𝑦
98, 3wceq 1331 . . . 4 wff 𝑦 = 𝐵
106, 9wa 103 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 3988 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1331 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
 Colors of variables: wff set class This definition is referenced by:  mpteq12f  4008  nfmpt  4020  nfmpt1  4021  cbvmptf  4022  cbvmpt  4023  mptv  4025  fconstmpt  4586  mptrel  4667  rnmpt  4787  resmpt  4867  mptresid  4873  mptcnv  4941  mptpreima  5032  funmpt  5161  dfmpt3  5245  mptfng  5248  mptun  5254  dffn5im  5467  fvmptss2  5496  fvmptg  5497  fndmin  5527  f1ompt  5571  fmptco  5586  mpomptx  5862  f1ocnvd  5972  f1od2  6132  dftpos4  6160  mapsncnv  6589
 Copyright terms: Public domain W3C validator