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 4763
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 4762 . 2 class (𝑥𝐴𝐵)
51cv 1522 . . . . 5 class 𝑥
65, 2wcel 2030 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1522 . . . . 5 class 𝑦
98, 3wceq 1523 . . . 4 wff 𝑦 = 𝐵
106, 9wa 383 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4745 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1523 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  mpteq12f  4764  mpteq12d  4767  mpteq12df  4768  nfmpt  4779  nfmpt1  4780  cbvmptf  4781  cbvmpt  4782  mptv  4784  csbmpt12  5039  dfid4  5055  fconstmpt  5197  mptrel  5281  rnmpt  5403  resmpt  5484  mptresid  5491  mptcnv  5569  mptpreima  5666  funmpt  5964  dfmpt3  6052  mptfnf  6053  mptfng  6057  mptun  6063  dffn5  6280  feqmptdf  6290  fvmptg  6319  fvmptndm  6347  fndmin  6364  f1ompt  6422  fmptco  6436  fmptsng  6475  fmptsnd  6476  mpt2mptx  6793  f1ocnvd  6926  dftpos4  7416  mpt2curryd  7440  mapsncnv  7946  marypha2lem3  8384  cardf2  8807  aceq3lem  8981  compsscnv  9231  pjfval2  20101  2ndcdisj  21307  xkocnv  21665  abrexexd  29473  f1o3d  29559  fmptcof2  29585  mptssALT  29602  mpt2mptxf  29605  f1od2  29627  qqhval2  30154  dfbigcup2  32131  bj-0nelmpt  33194  bj-mpt2mptALT  33197  rnmptsn  33312  curf  33517  curunc  33521  phpreu  33523  poimirlem26  33565  mbfposadd  33587  fnopabco  33647  mptbi12f  34105  fgraphopab  38105  mptssid  39764  dfafn5a  41561  mpt2mptx2  42438
  Copyright terms: Public domain W3C validator