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 5111
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 5110 . 2 class (𝑥𝐴𝐵)
51cv 1537 . . . . 5 class 𝑥
65, 2wcel 2111 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1537 . . . . 5 class 𝑦
98, 3wceq 1538 . . . 4 wff 𝑦 = 𝐵
106, 9wa 399 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 5092 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1538 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12df  5112  mpteq12f  5113  nfmpt  5127  nfmpt1  5128  cbvmptf  5129  cbvmptfg  5130  mptv  5135  csbmpt12  5409  dfid4  5426  fconstmpt  5578  mptrel  5661  rnmpt  5791  resmpt  5872  mptresid  5885  mptresidOLD  5887  mptcnv  5965  mptpreima  6059  funmpt  6362  dfmpt3  6454  mptfnf  6455  mptfng  6459  mptun  6466  dffn5  6699  feqmptdf  6710  fvmptg  6743  fvmptndm  6775  fndmin  6792  f1ompt  6852  fmptco  6868  fmptsng  6907  fmptsnd  6908  mpomptx  7244  f1ocnvd  7376  dftpos4  7894  mpocurryd  7918  mapsncnv  8440  marypha2lem3  8885  cardf2  9356  aceq3lem  9531  compsscnv  9782  pjfval2  20398  2ndcdisj  22061  xkocnv  22419  abrexexd  30277  f1o3d  30386  fmptcof2  30420  mptssALT  30438  mpomptxf  30442  f1od2  30483  qqhval2  31333  dfbigcup2  33473  bj-0nelmpt  34531  bj-mpomptALT  34534  rnmptsn  34752  curf  35035  curunc  35039  phpreu  35041  poimirlem26  35083  mbfposadd  35104  fnopabco  35161  mptbi12f  35604  fgraphopab  40152  mptssid  41875  dfafn5a  43714  mpomptx2  44734
  Copyright terms: Public domain W3C validator