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

Definition df-mpt 4924
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 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cmpt 4923 . 2 class (𝑥𝐴𝐵)
51cv 1636 . . . . 5 class 𝑥
65, 2wcel 2156 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1636 . . . . 5 class 𝑦
98, 3wceq 1637 . . . 4 wff 𝑦 = 𝐵
106, 9wa 384 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4906 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1637 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4925  mpteq12d  4928  mpteq12df  4929  nfmpt  4940  nfmpt1  4941  cbvmptf  4942  cbvmpt  4943  mptv  4945  csbmpt12  5205  dfid4  5221  fconstmpt  5363  mptrel  5450  rnmpt  5572  resmpt  5654  mptresid  5668  mptcnv  5745  mptpreima  5842  funmpt  6135  dfmpt3  6221  mptfnf  6222  mptfng  6226  mptun  6232  dffn5  6458  feqmptdf  6468  fvmptg  6497  fvmptndm  6525  fndmin  6542  f1ompt  6599  fmptco  6615  fmptsng  6655  fmptsnd  6656  mpt2mptx  6977  f1ocnvd  7110  dftpos4  7602  mpt2curryd  7626  mapsncnv  8137  marypha2lem3  8578  cardf2  9048  aceq3lem  9222  compsscnv  9474  pjfval2  20259  2ndcdisj  21469  xkocnv  21827  abrexexd  29668  f1o3d  29754  fmptcof2  29780  mptssALT  29797  mpt2mptxf  29800  f1od2  29822  qqhval2  30347  dfbigcup2  32322  bj-0nelmpt  33375  bj-mpt2mptALT  33378  rnmptsn  33494  curf  33695  curunc  33699  phpreu  33701  poimirlem26  33743  mbfposadd  33764  fnopabco  33824  mptbi12f  34280  fgraphopab  38283  mptssid  39928  dfafn5a  41743  mpt2mptx2  42675
  Copyright terms: Public domain W3C validator