Definition df-mpt 5231

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

This definition is referenced by:  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  nfmpt  5254  nfmpt1  5255  cbvmptf  5256  cbvmptfg  5257  cbvmptv  5260  mptv  5263  csbmpt12  5566  dfid4  5583  fconstmpt  5750  mptrel  5837  rnmpt  5970  resmpt  6056  mptresid  6070  mptcnv  6161  mptpreima  6259  funmpt  6605  dfmpt3  6702  mptfnf  6703  mptfng  6707  mptun  6714  dffn5  6966  feqmptdf  6978  fvmptg  7013  fvmptndm  7046  fndmin  7064  f1ompt  7130  fmptco  7148  fmptsng  7187  fmptsnd  7188  mpomptx  7545  f1ocnvd  7683  dftpos4  8268  mpocurryd  8292  mapsncnv  8931  marypha2lem3  9474  cardf2  9980  aceq3lem  10157  compsscnv  10408  pjfval2  21746  2ndcdisj  23479  xkocnv  23837  dvcnp2  25969  dvmulbr  25989  dvcobr  25997  cmvth  26043  dvfsumle  26074  dvfsumlem2  26081  taylthlem2  26430  abrexexd  32536  f1o3d  32643  fmptcof2  32673  mptssALT  32691  mpomptxf  32693  f1od2  32738  qqhval2  33944  dfbigcup2  35880  cbvmptvw2  36216  cbvmptdavw  36249  cbvmptdavw2  36270  bj-0nelmpt  37098  bj-mpomptALT  37101  rnmptsn  37317  curf  37584  curunc  37588  phpreu  37590  poimirlem26  37632  mbfposadd  37653  fnopabco  37709  mptbi12f  38152  fgraphopab  43191  mptssid  45184  dfafn5a  47109  mpomptx2  48179