Definition df-mpt 5231

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

This definition is referenced by:  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  nfmpt  5254  nfmpt1  5255  cbvmptf  5256  cbvmptfg  5257  cbvmptv  5260  mptv  5263  csbmpt12  5556  dfid4  5574  fconstmpt  5736  mptrel  5823  rnmpt  5952  resmpt  6035  mptresid  6048  mptcnv  6136  mptpreima  6234  funmpt  6583  dfmpt3  6681  mptfnf  6682  mptfng  6686  mptun  6693  dffn5  6947  feqmptdf  6959  fvmptg  6993  fvmptndm  7025  fndmin  7043  f1ompt  7107  fmptco  7123  fmptsng  7162  fmptsnd  7163  mpomptx  7517  f1ocnvd  7653  dftpos4  8226  mpocurryd  8250  mapsncnv  8883  marypha2lem3  9428  cardf2  9934  aceq3lem  10111  compsscnv  10362  pjfval2  21255  2ndcdisj  22951  xkocnv  23309  abrexexd  31733  f1o3d  31838  fmptcof2  31869  mptssALT  31887  mpomptxf  31892  f1od2  31933  qqhval2  32950  dfbigcup2  34859  gg-dvcnp2  35162  gg-dvmulbr  35163  gg-dvcobr  35164  gg-cmvth  35169  gg-dvfsumle  35170  gg-dvfsumlem2  35171  bj-0nelmpt  35985  bj-mpomptALT  35988  rnmptsn  36204  curf  36454  curunc  36458  phpreu  36460  poimirlem26  36502  mbfposadd  36523  fnopabco  36579  mptbi12f  37022  fgraphopab  41937  mptssid  43929  dfafn5a  45854  mpomptx2  46963