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 4639
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 4637 . 2 class (𝑥𝐴𝐵)
51cv 1473 . . . . 5 class 𝑥
65, 2wcel 1976 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1473 . . . . 5 class 𝑦
98, 3wceq 1474 . . . 4 wff 𝑦 = 𝐵
106, 9wa 382 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4636 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1474 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4655  nfmpt  4668  nfmpt1  4669  cbvmptf  4670  cbvmpt  4671  mptv  4673  csbmpt12  4923  dfid4  4944  fconstmpt  5074  mptrel  5157  rnmpt  5278  resmpt  5355  mptresid  5361  mptcnv  5439  mptpreima  5530  funmpt  5825  dfmpt3  5912  mptfnf  5913  mptfng  5917  mptun  5923  dffn5  6135  feqmptdf  6145  fvmptg  6173  fvmptndm  6200  fndmin  6216  f1ompt  6274  fmptco  6287  fmptsng  6316  fmptsnd  6317  mpt2mptx  6626  f1ocnvd  6759  dftpos4  7235  mpt2curryd  7259  mapsncnv  7767  marypha2lem3  8203  cardf2  8629  aceq3lem  8803  compsscnv  9053  pjfval2  19819  2ndcdisj  21016  xkocnv  21374  clwwlknprop  26093  abrexexd  28524  f1o3d  28606  mpteq12df  28630  fmptcof2  28632  mptssALT  28650  mpt2mptxf  28653  f1od2  28680  qqhval2  29147  mpteq12d  30708  dfbigcup2  30969  bj-0nelmpt  32033  bj-mpt2mptALT  32036  rnmptsn  32141  curf  32340  curunc  32344  phpreu  32346  poimirlem26  32388  mbfposadd  32410  fnopabco  32470  mptbi12f  32928  fgraphopab  36590  dfafn5a  39673  mpt2mptx2  41887
  Copyright terms: Public domain W3C validator