Definition df-mpt 5191

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 5190	. 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 5171	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1570	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12da  5192  mpteq12f  5194  mpteq12dva  5195  nfmpt  5207  nfmpt1  5208  cbvmptf  5209  cbvmptfg  5210  cbvmptv  5213  mptv  5215  csbmpt12  5540  dfid4  5555  fconstmpt  5721  mptrel  5810  rnmpt  5945  resmpt  6037  mptresid  6051  mptcnv  6136  mptpreima  6238  funmpt  6575  dfmpt3  6670  mptfnf  6671  mptfng  6675  mptun  6682  dffn5  6940  feqmptdf  6952  fvmptg  6988  fvmptndm  7022  fndmin  7041  f1ompt  7107  fmptco  7126  fmptsng  7169  fmptsnd  7170  mpomptx  7529  f1ocnvd  7668  dftpos4  8246  mpocurryd  8270  curf  8872  mapsncnv  8903  marypha2lem3  9410  cardf2  9951  aceq3lem  10126  compsscnv  10376  pjfval2  21923  2ndcdisj  23683  xkocnv  24041  dvcnp2  26149  dvmulbr  26168  dvcobr  26175  cmvth  26220  dvfsumle  26250  dvfsumlem2  26256  taylthlem2  26607  abrexexd  32970  f1o3d  33086  fmptcof2  33117  mptssALT  33134  mpomptxf  33138  f1od2  33177  qqhval2  34479  dfbigcup2  36463  cbvmptvw2  36841  cbvmptdavw  36874  cbvmptdavw2  36895  bj-0nelmpt  37853  bj-mpomptALT  37856  rnmptsn  38076  curunc  38343  phpreu  38345  poimirlem26  38382  mbfposadd  38403  fnopabco  38460  mptbi12f  38901  dfqmap3  39183  blockadjliftmap  39193  fgraphopab  44031  mptssid  46057  lambert0  47742  lamberte  47743  sinnpoly  47746  dfafn5a  48035  mpomptx2  49252