Definition df-mpt 5192

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 5191	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1568	. . . . 5 class 𝑥
6	5, 2	wcel 2142	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1568	. . . . 5 class 𝑦
9	8, 3	wceq 1569	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5172	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1569	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12da  5193  mpteq12f  5195  mpteq12dva  5196  nfmpt  5208  nfmpt1  5209  cbvmptf  5210  cbvmptfg  5211  cbvmptv  5214  mptv  5216  csbmpt12  5541  dfid4  5556  fconstmpt  5722  mptrel  5811  rnmpt  5946  resmpt  6038  mptresid  6052  mptcnv  6137  mptpreima  6238  funmpt  6574  dfmpt3  6669  mptfnf  6670  mptfng  6674  mptun  6681  dffn5  6939  feqmptdf  6951  fvmptg  6987  fvmptndm  7021  fndmin  7040  f1ompt  7106  fmptco  7125  fmptsng  7166  fmptsnd  7167  mpomptx  7525  f1ocnvd  7663  dftpos4  8239  mpocurryd  8263  mapsncnv  8889  marypha2lem3  9395  cardf2  9936  aceq3lem  10111  compsscnv  10361  pjfval2  21870  2ndcdisj  23624  xkocnv  23982  dvcnp2  26090  dvmulbr  26109  dvcobr  26116  cmvth  26161  dvfsumle  26191  dvfsumlem2  26197  taylthlem2  26548  abrexexd  32866  f1o3d  32982  fmptcof2  33013  mptssALT  33030  mpomptxf  33034  f1od2  33075  qqhval2  34381  dfbigcup2  36397  cbvmptvw2  36774  cbvmptdavw  36807  cbvmptdavw2  36828  bj-0nelmpt  37786  bj-mpomptALT  37789  rnmptsn  38009  curf  38277  curunc  38281  phpreu  38283  poimirlem26  38325  mbfposadd  38346  fnopabco  38402  mptbi12f  38843  dfqmap3  39125  blockadjliftmap  39135  fgraphopab  43958  mptssid  45984  lambert0  47652  lamberte  47653  sinnpoly  47656  dfafn5a  47925  mpomptx2  49143