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 4685
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 4683 . 2 class (𝑥𝐴𝐵)
51cv 1479 . . . . 5 class 𝑥
65, 2wcel 1987 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1479 . . . . 5 class 𝑦
98, 3wceq 1480 . . . 4 wff 𝑦 = 𝐵
106, 9wa 384 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4682 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1480 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4701  mpteq12d  4704  mpteq12df  4705  nfmpt  4716  nfmpt1  4717  cbvmptf  4718  cbvmpt  4719  mptv  4721  csbmpt12  4980  dfid4  5001  fconstmpt  5133  mptrel  5218  rnmpt  5341  resmpt  5418  mptresid  5425  mptcnv  5503  mptpreima  5597  funmpt  5894  dfmpt3  5981  mptfnf  5982  mptfng  5986  mptun  5992  dffn5  6208  feqmptdf  6218  fvmptg  6247  fvmptndm  6274  fndmin  6290  f1ompt  6348  fmptco  6362  fmptsng  6399  fmptsnd  6400  mpt2mptx  6716  f1ocnvd  6849  dftpos4  7331  mpt2curryd  7355  mapsncnv  7864  marypha2lem3  8303  cardf2  8729  aceq3lem  8903  compsscnv  9153  pjfval2  19993  2ndcdisj  21199  xkocnv  21557  abrexexd  29235  f1o3d  29316  fmptcof2  29340  mptssALT  29358  mpt2mptxf  29361  f1od2  29383  qqhval2  29850  dfbigcup2  31701  bj-0nelmpt  32745  bj-mpt2mptALT  32748  rnmptsn  32853  curf  33058  curunc  33062  phpreu  33064  poimirlem26  33106  mbfposadd  33128  fnopabco  33188  mptbi12f  33646  fgraphopab  37308  mptssid  38960  dfafn5a  40574  mpt2mptx2  41431
  Copyright terms: Public domain W3C validator