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 5139
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 5138 . 2 class (𝑥𝐴𝐵)
51cv 1527 . . . . 5 class 𝑥
65, 2wcel 2105 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1527 . . . . 5 class 𝑦
98, 3wceq 1528 . . . 4 wff 𝑦 = 𝐵
106, 9wa 396 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 5120 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1528 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12df  5140  mpteq12f  5141  nfmpt  5155  nfmpt1  5156  cbvmptf  5157  cbvmptfg  5158  mptv  5163  csbmpt12  5436  dfid4  5455  fconstmpt  5608  mptrel  5691  rnmpt  5821  resmpt  5899  mptresid  5912  mptresidOLD  5914  mptcnv  5992  mptpreima  6086  funmpt  6387  dfmpt3  6476  mptfnf  6477  mptfng  6481  mptun  6488  dffn5  6718  feqmptdf  6729  fvmptg  6760  fvmptndm  6791  fndmin  6808  f1ompt  6868  fmptco  6884  fmptsng  6923  fmptsnd  6924  mpomptx  7254  f1ocnvd  7385  dftpos4  7902  mpocurryd  7926  mapsncnv  8446  marypha2lem3  8890  cardf2  9361  aceq3lem  9535  compsscnv  9782  pjfval2  20783  2ndcdisj  21994  xkocnv  22352  abrexexd  30197  f1o3d  30301  fmptcof2  30331  mptssALT  30349  mpomptxf  30354  f1od2  30384  qqhval2  31123  dfbigcup2  33258  bj-0nelmpt  34301  bj-mpomptALT  34304  rnmptsn  34499  curf  34752  curunc  34756  phpreu  34758  poimirlem26  34800  mbfposadd  34821  fnopabco  34881  mptbi12f  35327  fgraphopab  39690  mptssid  41391  dfafn5a  43240  mpomptx2  44281
  Copyright terms: Public domain W3C validator