Definition df-mpt 5184

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 5183	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1561	. . . . 5 class 𝑥
6	5, 2	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1561	. . . . 5 class 𝑦
9	8, 3	wceq 1562	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5164	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1562	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  nfmpt  5200  nfmpt1  5201  cbvmptf  5202  cbvmptfg  5203  cbvmptv  5206  mptv  5208  csbmpt12  5530  dfid4  5545  fconstmpt  5711  mptrel  5800  rnmpt  5935  resmpt  6028  mptresid  6042  mptcnv  6127  mptpreima  6227  funmpt  6561  dfmpt3  6657  mptfnf  6658  mptfng  6662  mptun  6669  dffn5  6927  feqmptdf  6939  fvmptg  6975  fvmptndm  7009  fndmin  7028  f1ompt  7094  fmptco  7113  fmptsng  7154  fmptsnd  7155  mpomptx  7511  f1ocnvd  7649  dftpos4  8227  mpocurryd  8251  mapsncnv  8877  marypha2lem3  9385  cardf2  9903  aceq3lem  10078  compsscnv  10330  pjfval2  21763  2ndcdisj  23518  xkocnv  23876  dvcnp2  25984  dvmulbr  26003  dvcobr  26010  cmvth  26055  dvfsumle  26085  dvfsumlem2  26091  taylthlem2  26439  abrexexd  32710  f1o3d  32830  fmptcof2  32861  mptssALT  32878  mpomptxf  32882  f1od2  32923  qqhval2  34281  dfbigcup2  36252  cbvmptvw2  36599  cbvmptdavw  36632  cbvmptdavw2  36653  bj-0nelmpt  37611  bj-mpomptALT  37614  rnmptsn  37834  curf  38102  curunc  38106  phpreu  38108  poimirlem26  38150  mbfposadd  38171  fnopabco  38227  mptbi12f  38670  dfqmap3  38952  blockadjliftmap  38962  fgraphopab  43785  mptssid  45821  lambert0  47486  lamberte  47487  sinnpoly  47490  dfafn5a  47759  mpomptx2  48962