Definition df-mpt 5181

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 5180	. 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 5161	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1542	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5182  mpteq12f  5184  mpteq12dva  5185  nfmpt  5197  nfmpt1  5198  cbvmptf  5199  cbvmptfg  5200  cbvmptv  5203  mptv  5205  csbmpt12  5506  dfid4  5521  fconstmpt  5687  mptrel  5775  rnmpt  5907  resmpt  5997  mptresid  6011  mptcnv  6097  mptpreima  6197  funmpt  6531  dfmpt3  6627  mptfnf  6628  mptfng  6632  mptun  6639  dffn5  6893  feqmptdf  6905  fvmptg  6940  fvmptndm  6974  fndmin  6992  f1ompt  7058  fmptco  7076  fmptsng  7116  fmptsnd  7117  mpomptx  7473  f1ocnvd  7611  dftpos4  8189  mpocurryd  8213  mapsncnv  8835  marypha2lem3  9344  cardf2  9859  aceq3lem  10034  compsscnv  10285  pjfval2  21668  2ndcdisj  23404  xkocnv  23762  dvcnp2  25881  dvmulbr  25901  dvcobr  25909  cmvth  25955  dvfsumle  25986  dvfsumlem2  25993  taylthlem2  26342  abrexexd  32587  f1o3d  32707  fmptcof2  32738  mptssALT  32755  mpomptxf  32759  f1od2  32800  qqhval2  34141  dfbigcup2  36093  cbvmptvw2  36430  cbvmptdavw  36463  cbvmptdavw2  36484  bj-0nelmpt  37323  bj-mpomptALT  37326  rnmptsn  37542  curf  37801  curunc  37805  phpreu  37807  poimirlem26  37849  mbfposadd  37870  fnopabco  37926  mptbi12f  38369  dfqmap3  38651  blockadjliftmap  38661  fgraphopab  43512  mptssid  45552  lambert0  47200  lamberte  47201  sinnpoly  47204  dfafn5a  47473  mpomptx2  48648