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 5226
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 5225 . 2 class (𝑥𝐴𝐵)
51cv 1539 . . . . 5 class 𝑥
65, 2wcel 2108 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1539 . . . . 5 class 𝑦
98, 3wceq 1540 . . . 4 wff 𝑦 = 𝐵
106, 9wa 395 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 5205 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1540 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12da  5227  mpteq12dfOLD  5229  mpteq12f  5230  mpteq12dva  5231  nfmpt  5249  nfmpt1  5250  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  mptv  5258  csbmpt12  5562  dfid4  5579  fconstmpt  5747  mptrel  5835  rnmpt  5968  resmpt  6055  mptresid  6069  mptcnv  6159  mptpreima  6258  funmpt  6604  dfmpt3  6702  mptfnf  6703  mptfng  6707  mptun  6714  dffn5  6967  feqmptdf  6979  fvmptg  7014  fvmptndm  7047  fndmin  7065  f1ompt  7131  fmptco  7149  fmptsng  7188  fmptsnd  7189  mpomptx  7546  f1ocnvd  7684  dftpos4  8270  mpocurryd  8294  mapsncnv  8933  marypha2lem3  9477  cardf2  9983  aceq3lem  10160  compsscnv  10411  pjfval2  21729  2ndcdisj  23464  xkocnv  23822  dvcnp2  25955  dvmulbr  25975  dvcobr  25983  cmvth  26029  dvfsumle  26060  dvfsumlem2  26067  taylthlem2  26416  abrexexd  32528  f1o3d  32637  fmptcof2  32667  mptssALT  32685  mpomptxf  32687  f1od2  32732  qqhval2  33983  dfbigcup2  35900  cbvmptvw2  36235  cbvmptdavw  36268  cbvmptdavw2  36289  bj-0nelmpt  37117  bj-mpomptALT  37120  rnmptsn  37336  curf  37605  curunc  37609  phpreu  37611  poimirlem26  37653  mbfposadd  37674  fnopabco  37730  mptbi12f  38173  fgraphopab  43215  mptssid  45247  dfafn5a  47172  mpomptx2  48251
  Copyright terms: Public domain W3C validator