Definition df-mpt 5156

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

This definition is referenced by:  mpteq12da  5157  mpteq12f  5159  mpteq12dva  5160  nfmpt  5172  nfmpt1  5173  cbvmptf  5174  cbvmptfg  5175  cbvmptv  5178  mptv  5180  csbmpt12  5501  dfid4  5516  fconstmpt  5682  mptrel  5770  rnmpt  5901  resmpt  5991  mptresid  6005  mptcnv  6091  mptpreima  6191  funmpt  6525  dfmpt3  6621  mptfnf  6622  mptfng  6626  mptun  6633  dffn5  6887  feqmptdf  6899  fvmptg  6934  fvmptndm  6968  fndmin  6986  f1ompt  7052  fmptco  7071  fmptsng  7112  fmptsnd  7113  mpomptx  7469  f1ocnvd  7607  dftpos4  8184  mpocurryd  8208  mapsncnv  8830  marypha2lem3  9339  cardf2  9856  aceq3lem  10031  compsscnv  10282  pjfval2  21678  2ndcdisj  23409  xkocnv  23767  dvcnp2  25875  dvmulbr  25894  dvcobr  25901  cmvth  25946  dvfsumle  25976  dvfsumlem2  25982  taylthlem2  26327  abrexexd  32567  f1o3d  32687  fmptcof2  32718  mptssALT  32735  mpomptxf  32739  f1od2  32780  qqhval2  34114  dfbigcup2  36067  cbvmptvw2  36404  cbvmptdavw  36437  cbvmptdavw2  36458  bj-0nelmpt  37416  bj-mpomptALT  37419  rnmptsn  37639  curf  37907  curunc  37911  phpreu  37913  poimirlem26  37955  mbfposadd  37976  fnopabco  38032  mptbi12f  38475  dfqmap3  38757  blockadjliftmap  38767  fgraphopab  43619  mptssid  45658  lambert0  47323  lamberte  47324  sinnpoly  47327  dfafn5a  47596  mpomptx2  48799