Definition df-mpt 5226

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

This definition is referenced by:  mpteq12da  5227  mpteq12dfOLD  5229  mpteq12f  5230  mpteq12dva  5231  nfmpt  5249  nfmpt1  5250  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  mptv  5258  csbmpt12  5562  dfid4  5579  fconstmpt  5747  mptrel  5835  rnmpt  5968  resmpt  6055  mptresid  6069  mptcnv  6159  mptpreima  6258  funmpt  6604  dfmpt3  6702  mptfnf  6703  mptfng  6707  mptun  6714  dffn5  6967  feqmptdf  6979  fvmptg  7014  fvmptndm  7047  fndmin  7065  f1ompt  7131  fmptco  7149  fmptsng  7188  fmptsnd  7189  mpomptx  7546  f1ocnvd  7684  dftpos4  8270  mpocurryd  8294  mapsncnv  8933  marypha2lem3  9477  cardf2  9983  aceq3lem  10160  compsscnv  10411  pjfval2  21729  2ndcdisj  23464  xkocnv  23822  dvcnp2  25955  dvmulbr  25975  dvcobr  25983  cmvth  26029  dvfsumle  26060  dvfsumlem2  26067  taylthlem2  26416  abrexexd  32528  f1o3d  32637  fmptcof2  32667  mptssALT  32685  mpomptxf  32687  f1od2  32732  qqhval2  33983  dfbigcup2  35900  cbvmptvw2  36235  cbvmptdavw  36268  cbvmptdavw2  36289  bj-0nelmpt  37117  bj-mpomptALT  37120  rnmptsn  37336  curf  37605  curunc  37609  phpreu  37611  poimirlem26  37653  mbfposadd  37674  fnopabco  37730  mptbi12f  38173  fgraphopab  43215  mptssid  45247  dfafn5a  47172  mpomptx2  48251