Definition df-mpt 5156

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 5155	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1547	. . . . 5 class 𝑥
6	5, 2	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1547	. . . . 5 class 𝑦
9	8, 3	wceq 1548	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1548	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5157  mpteq12f  5159  mpteq12dva  5160  nfmpt  5172  nfmpt1  5173  cbvmptf  5174  cbvmptfg  5175  cbvmptv  5178  mptv  5180  csbmpt12  5501  dfid4  5516  fconstmpt  5682  mptrel  5770  rnmpt  5905  resmpt  5995  mptresid  6009  mptcnv  6094  mptpreima  6192  funmpt  6526  dfmpt3  6622  mptfnf  6623  mptfng  6627  mptun  6634  dffn5  6888  feqmptdf  6900  fvmptg  6936  fvmptndm  6970  fndmin  6989  f1ompt  7055  fmptco  7074  fmptsng  7115  fmptsnd  7116  mpomptx  7472  f1ocnvd  7610  dftpos4  8187  mpocurryd  8211  mapsncnv  8835  marypha2lem3  9344  cardf2  9862  aceq3lem  10037  compsscnv  10289  pjfval2  21687  2ndcdisj  23442  xkocnv  23800  dvcnp2  25908  dvmulbr  25927  dvcobr  25934  cmvth  25979  dvfsumle  26009  dvfsumlem2  26015  taylthlem2  26360  abrexexd  32599  f1o3d  32720  fmptcof2  32751  mptssALT  32768  mpomptxf  32772  f1od2  32813  qqhval2  34176  dfbigcup2  36138  cbvmptvw2  36475  cbvmptdavw  36508  cbvmptdavw2  36529  bj-0nelmpt  37487  bj-mpomptALT  37490  rnmptsn  37710  curf  37978  curunc  37982  phpreu  37984  poimirlem26  38026  mbfposadd  38047  fnopabco  38103  mptbi12f  38546  dfqmap3  38828  blockadjliftmap  38838  fgraphopab  43661  mptssid  45697  lambert0  47362  lamberte  47363  sinnpoly  47366  dfafn5a  47635  mpomptx2  48838