Definition df-mpt 5202

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 5201	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1539	. . . . 5 class 𝑥
6	5, 2	wcel 2108	. . . 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 5181	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1540	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5203  mpteq12f  5205  mpteq12dva  5206  nfmpt  5219  nfmpt1  5220  cbvmptf  5221  cbvmptfg  5222  cbvmptv  5225  mptv  5228  csbmpt12  5532  dfid4  5549  fconstmpt  5716  mptrel  5804  rnmpt  5937  resmpt  6024  mptresid  6038  mptcnv  6128  mptpreima  6227  funmpt  6573  dfmpt3  6671  mptfnf  6672  mptfng  6676  mptun  6683  dffn5  6936  feqmptdf  6948  fvmptg  6983  fvmptndm  7016  fndmin  7034  f1ompt  7100  fmptco  7118  fmptsng  7159  fmptsnd  7160  mpomptx  7518  f1ocnvd  7656  dftpos4  8242  mpocurryd  8266  mapsncnv  8905  marypha2lem3  9447  cardf2  9955  aceq3lem  10132  compsscnv  10383  pjfval2  21667  2ndcdisj  23392  xkocnv  23750  dvcnp2  25871  dvmulbr  25891  dvcobr  25899  cmvth  25945  dvfsumle  25976  dvfsumlem2  25983  taylthlem2  26332  abrexexd  32436  f1o3d  32551  fmptcof2  32581  mptssALT  32599  mpomptxf  32601  f1od2  32644  qqhval2  33959  dfbigcup2  35863  cbvmptvw2  36198  cbvmptdavw  36231  cbvmptdavw2  36252  bj-0nelmpt  37080  bj-mpomptALT  37083  rnmptsn  37299  curf  37568  curunc  37572  phpreu  37574  poimirlem26  37616  mbfposadd  37637  fnopabco  37693  mptbi12f  38136  fgraphopab  43174  mptssid  45213  lambert0  46867  lamberte  46868  dfafn5a  47137  mpomptx2  48258