Definition df-mpt 5250

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 5249	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1536	. . . . 5 class 𝑥
6	5, 2	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1536	. . . . 5 class 𝑦
9	8, 3	wceq 1537	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5228	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1537	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5251  mpteq12dfOLD  5253  mpteq12f  5254  mpteq12dva  5255  nfmpt  5273  nfmpt1  5274  cbvmptf  5275  cbvmptfg  5276  cbvmptv  5279  mptv  5282  csbmpt12  5576  dfid4  5594  fconstmpt  5762  mptrel  5849  rnmpt  5980  resmpt  6066  mptresid  6080  mptcnv  6171  mptpreima  6269  funmpt  6616  dfmpt3  6714  mptfnf  6715  mptfng  6719  mptun  6726  dffn5  6980  feqmptdf  6992  fvmptg  7027  fvmptndm  7060  fndmin  7078  f1ompt  7145  fmptco  7163  fmptsng  7202  fmptsnd  7203  mpomptx  7563  f1ocnvd  7701  dftpos4  8286  mpocurryd  8310  mapsncnv  8951  marypha2lem3  9506  cardf2  10012  aceq3lem  10189  compsscnv  10440  pjfval2  21752  2ndcdisj  23485  xkocnv  23843  dvcnp2  25975  dvmulbr  25995  dvcobr  26003  cmvth  26049  dvfsumle  26080  dvfsumlem2  26087  taylthlem2  26434  abrexexd  32537  f1o3d  32646  fmptcof2  32675  mptssALT  32693  mpomptxf  32695  f1od2  32735  qqhval2  33928  dfbigcup2  35863  cbvmptvw2  36200  cbvmptdavw  36233  cbvmptdavw2  36254  bj-0nelmpt  37082  bj-mpomptALT  37085  rnmptsn  37301  curf  37558  curunc  37562  phpreu  37564  poimirlem26  37606  mbfposadd  37627  fnopabco  37683  mptbi12f  38126  fgraphopab  43164  mptssid  45149  dfafn5a  47075  mpomptx2  48059