Definition df-mpt 5187

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 5186	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1569	. . . . 5 class 𝑥
6	5, 2	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1569	. . . . 5 class 𝑦
9	8, 3	wceq 1570	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5167	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1570	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  nfmpt  5203  nfmpt1  5204  cbvmptf  5205  cbvmptfg  5206  cbvmptv  5209  mptv  5211  csbmpt12  5536  dfid4  5551  fconstmpt  5717  mptrel  5806  rnmpt  5941  resmpt  6033  mptresid  6047  mptcnv  6132  mptpreima  6234  funmpt  6571  dfmpt3  6666  mptfnf  6667  mptfng  6671  mptun  6678  dffn5  6936  feqmptdf  6948  fvmptg  6984  fvmptndm  7018  fndmin  7037  f1ompt  7104  fmptco  7123  fmptsng  7166  fmptsnd  7167  mpomptx  7526  f1ocnvd  7665  dftpos4  8243  mpocurryd  8267  curf  8869  mapsncnv  8900  marypha2lem3  9407  cardf2  9948  aceq3lem  10123  compsscnv  10373  pjfval2  21922  2ndcdisj  23682  xkocnv  24040  dvcnp2  26147  dvmulbr  26166  dvcobr  26173  cmvth  26218  dvfsumle  26248  dvfsumlem2  26254  taylthlem2  26610  abrexexd  32984  f1o3d  33099  fmptcof2  33130  mptssALT  33147  mpomptxf  33151  f1od2  33190  qqhval2  34492  dfbigcup2  36476  cbvmptvw2  36854  cbvmptdavw  36887  cbvmptdavw2  36908  bj-0nelmpt  37866  bj-mpomptALT  37869  rnmptsn  38089  curunc  38356  phpreu  38358  poimirlem26  38395  mbfposadd  38416  fnopabco  38473  mptbi12f  38914  dfqmap3  39196  blockadjliftmap  39206  fgraphopab  44044  mptssid  46070  lambert0  47755  lamberte  47756  sinnpoly  47759  dfafn5a  48048  mpomptx2  49265