MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpt Structured version   GIF version

Definition df-mpt 4353
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 𝑥. An example is the square function for complex numbers, (𝑥 ∈ ℂ ↦ (𝑥↑2)). 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 set 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cmpt 4351 . 2 class (𝑥𝐴𝐵)
51cv 1661 . . . . 5 class 𝑥
65, 2wcel 1734 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 set 𝑦
87cv 1661 . . . . 5 class 𝑦
98, 3wceq 1662 . . . 4 wff 𝑦 = 𝐵
106, 9wa 360 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4350 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1662 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  4369  nfmpt  4381  nfmpt1  4382  cbvmpt  4383  mptv  4385  fconstmpt  5012  rnmpt  5210  resmpt  5286  mptresid  5290  mptpreima  5461  funmpt  5588  dfmpt3  5666  mptfng  5669  mptun  5674  dffn5  5872  fvmptg  5904  fndmin  5937  f1ompt  5991  fmptco  6001  mpt2mptx  6266  f1ocnvd  6395  dftpos4  6602  mapsncnv  7155  marypha2lem3  7537  cardf2  7927  aceq3lem  8098  compsscnv  8348  fsumrev  12682  fsumshft  12683  pjfval2  17068  2ndcdisj  17651  pt1hmeo  17970  xkocnv  17978  abrexexd  24127  f1o3d  24189  mptcnv  24193  cbvmptf  24216  mptfnf  24221  feqmptdf  24223  fmptcof2  24224  mpt2mptxf  24240  f1od2  24269  qqhval2  24709  dfid4  25640  fprodshft  25757  fprodrev  25758  mptrel  25849  mpteq12d  25853  dfbigcup2  26201  fnopabco  26880  mptbi12f  27206  fgraphopab  28028  dfafn5a  28519  elovmpt3rab1  28624  clwwlknprop  29119
  Copyright terms: Public domain W3C validator