Definition df-mpt 5173

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

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	cmpt 5172	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1540	. . . . 5 class 𝑥
6	5, 2	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1540	. . . . 5 class 𝑦
9	8, 3	wceq 1541	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5153	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1541	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5174  mpteq12f  5176  mpteq12dva  5177  nfmpt  5189  nfmpt1  5190  cbvmptf  5191  cbvmptfg  5192  cbvmptv  5195  mptv  5197  csbmpt12  5497  dfid4  5512  fconstmpt  5678  mptrel  5765  rnmpt  5897  resmpt  5986  mptresid  6000  mptcnv  6086  mptpreima  6185  funmpt  6519  dfmpt3  6615  mptfnf  6616  mptfng  6620  mptun  6627  dffn5  6880  feqmptdf  6892  fvmptg  6927  fvmptndm  6960  fndmin  6978  f1ompt  7044  fmptco  7062  fmptsng  7102  fmptsnd  7103  mpomptx  7459  f1ocnvd  7597  dftpos4  8175  mpocurryd  8199  mapsncnv  8817  marypha2lem3  9321  cardf2  9833  aceq3lem  10008  compsscnv  10259  pjfval2  21644  2ndcdisj  23369  xkocnv  23727  dvcnp2  25846  dvmulbr  25866  dvcobr  25874  cmvth  25920  dvfsumle  25951  dvfsumlem2  25958  taylthlem2  26307  abrexexd  32484  f1o3d  32603  fmptcof2  32634  mptssALT  32652  mpomptxf  32654  f1od2  32697  qqhval2  33990  dfbigcup2  35932  cbvmptvw2  36267  cbvmptdavw  36300  cbvmptdavw2  36321  bj-0nelmpt  37149  bj-mpomptALT  37152  rnmptsn  37368  curf  37637  curunc  37641  phpreu  37643  poimirlem26  37685  mbfposadd  37706  fnopabco  37762  mptbi12f  38205  fgraphopab  43235  mptssid  45277  lambert0  46917  lamberte  46918  sinnpoly  46921  dfafn5a  47190  mpomptx2  48365