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 5231
Description: Define maps-to notation for defining a function via a rule. Read as "the function which maps 𝑥 (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 5230 . 2 class (𝑥𝐴𝐵)
51cv 1540 . . . . 5 class 𝑥
65, 2wcel 2106 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1540 . . . . 5 class 𝑦
98, 3wceq 1541 . . . 4 wff 𝑦 = 𝐵
106, 9wa 396 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 5209 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1541 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  nfmpt  5254  nfmpt1  5255  cbvmptf  5256  cbvmptfg  5257  cbvmptv  5260  mptv  5263  csbmpt12  5556  dfid4  5574  fconstmpt  5736  mptrel  5823  rnmpt  5952  resmpt  6035  mptresid  6048  mptcnv  6136  mptpreima  6234  funmpt  6583  dfmpt3  6681  mptfnf  6682  mptfng  6686  mptun  6693  dffn5  6947  feqmptdf  6959  fvmptg  6993  fvmptndm  7025  fndmin  7043  f1ompt  7107  fmptco  7123  fmptsng  7162  fmptsnd  7163  mpomptx  7517  f1ocnvd  7653  dftpos4  8226  mpocurryd  8250  mapsncnv  8883  marypha2lem3  9428  cardf2  9934  aceq3lem  10111  compsscnv  10362  pjfval2  21255  2ndcdisj  22951  xkocnv  23309  abrexexd  31733  f1o3d  31838  fmptcof2  31869  mptssALT  31887  mpomptxf  31892  f1od2  31933  qqhval2  32950  dfbigcup2  34859  gg-dvcnp2  35162  gg-dvmulbr  35163  gg-dvcobr  35164  gg-cmvth  35169  gg-dvfsumle  35170  gg-dvfsumlem2  35171  bj-0nelmpt  35985  bj-mpomptALT  35988  rnmptsn  36204  curf  36454  curunc  36458  phpreu  36460  poimirlem26  36502  mbfposadd  36523  fnopabco  36579  mptbi12f  37022  fgraphopab  41937  mptssid  43929  dfafn5a  45854  mpomptx2  46963
  Copyright terms: Public domain W3C validator