MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpt Structured version   GIF version

Definition df-mpt 4299
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 set 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cmpt 4297 . 2 class (𝑥𝐴𝐵)
51cv 1653 . . . . 5 class 𝑥
65, 2wcel 1728 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 set 𝑦
87cv 1653 . . . . 5 class 𝑦
98, 3wceq 1654 . . . 4 wff 𝑦 = 𝐵
106, 9wa 360 . . 3 wff (𝑥𝐴𝑦 = 𝐵)
1110, 1, 7copab 4296 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
124, 11wceq 1654 1 wff (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
Colors of variables: wff set class
This definition is referenced by:  mpteq12f  4316  nfmpt  4328  nfmpt1  4329  cbvmpt  4330  mptv  4332  fconstmpt  4956  rnmpt  5151  resmpt  5226  mptresid  5230  mptpreima  5398  funmpt  5524  dfmpt3  5602  mptfng  5605  mptun  5610  dffn5  5808  fvmptg  5840  fndmin  5873  f1ompt  5927  fmptco  5937  mpt2mptx  6200  f1ocnvd  6329  dftpos4  6534  mapsncnv  7096  marypha2lem3  7478  cardf2  7868  aceq3lem  8039  compsscnv  8289  fsumrev  12600  fsumshft  12601  pjfval2  16974  2ndcdisj  17557  pt1hmeo  17876  xkocnv  17884  abrexexd  24026  f1o3d  24076  mptcnv  24080  cbvmptf  24103  mptfnf  24108  feqmptdf  24110  fmptcof2  24111  qqhval2  24401  dfid4  25218  fprodshft  25335  fprodrev  25336  mptrel  25427  mpteq12d  25431  dfbigcup2  25779  fnopabco  26466  mptbi12f  26794  fgraphopab  27618  dfafn5a  28112  elovmpt3rab1  28205
  Copyright terms: Public domain W3C validator