Definition df-mpt 5186

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

This definition is used by:  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  nfmpt  5202  nfmpt1  5203  cbvmptf  5204  cbvmptfg  5205  cbvmptv  5208  mptv  5210  csbmpt12  5528  dfid4  5543  fconstmpt  5709  mptrel  5799  rnmpt  5935  resmpt  6027  mptresid  6041  mptcnv  6126  mptpreima  6228  funmpt  6566  dfmpt3  6661  mptfnf  6662  mptfng  6666  mptun  6673  dffn5  6931  feqmptdf  6943  fvmptg  6979  fvmptndm  7013  fndmin  7032  f1ompt  7099  fmptco  7118  fmptsng  7161  fmptsnd  7162  mpomptx  7521  f1ocnvd  7660  mpt3mpt  7673  dftpos4  8240  mpocurryd  8264  curf  8868  mapsncnv  8899  marypha2lem3  9407  cardf2  9995  aceq3lem  10170  compsscnv  10420  pjfval2  21976  2ndcdisj  23736  xkocnv  24094  dvcnp2  26201  dvmulbr  26220  dvcobr  26227  cmvth  26272  dvfsumle  26302  dvfsumlem2  26308  taylthlem2  26664  abrexexd  33038  f1o3d  33153  fmptcof2  33184  mptssALT  33201  mpomptxf  33205  f1od2  33244  qqhval2  34547  dfbigcup2  36583  cbvmptvw2  36945  cbvmptdavw  36978  cbvmptdavw2  36999  bj-0nelmpt  37957  bj-mpomptALT  37960  rnmptsn  38178  curunc  38445  phpreu  38447  poimirlem26  38484  mbfposadd  38505  fnopabco  38577  mptbi12f  39018  dfqmap3  39300  blockadjliftmap  39310  fgraphopab  44148  mptssid  46174  lambert0  47859  lamberte  47860  sinnpoly  47863  dfafn5a  48152  mpomptx2  49369