Definition df-mpt 5177

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

This definition is referenced by:  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  nfmpt  5193  nfmpt1  5194  cbvmptf  5195  cbvmptfg  5196  cbvmptv  5199  mptv  5201  csbmpt12  5504  dfid4  5519  fconstmpt  5685  mptrel  5772  rnmpt  5903  resmpt  5992  mptresid  6006  mptcnv  6092  mptpreima  6191  funmpt  6524  dfmpt3  6620  mptfnf  6621  mptfng  6625  mptun  6632  dffn5  6885  feqmptdf  6897  fvmptg  6932  fvmptndm  6965  fndmin  6983  f1ompt  7049  fmptco  7067  fmptsng  7108  fmptsnd  7109  mpomptx  7466  f1ocnvd  7604  dftpos4  8185  mpocurryd  8209  mapsncnv  8827  marypha2lem3  9346  cardf2  9858  aceq3lem  10033  compsscnv  10284  pjfval2  21634  2ndcdisj  23359  xkocnv  23717  dvcnp2  25837  dvmulbr  25857  dvcobr  25865  cmvth  25911  dvfsumle  25942  dvfsumlem2  25949  taylthlem2  26298  abrexexd  32471  f1o3d  32584  fmptcof2  32614  mptssALT  32632  mpomptxf  32634  f1od2  32677  qqhval2  33948  dfbigcup2  35872  cbvmptvw2  36207  cbvmptdavw  36240  cbvmptdavw2  36261  bj-0nelmpt  37089  bj-mpomptALT  37092  rnmptsn  37308  curf  37577  curunc  37581  phpreu  37583  poimirlem26  37625  mbfposadd  37646  fnopabco  37702  mptbi12f  38145  fgraphopab  43176  mptssid  45219  lambert0  46872  lamberte  46873  sinnpoly  46876  dfafn5a  47145  mpomptx2  48320