Definition df-mpt 5232

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

This definition is referenced by:  mpteq12da  5233  mpteq12dfOLD  5235  mpteq12f  5236  mpteq12dva  5237  nfmpt  5255  nfmpt1  5256  cbvmptf  5257  cbvmptfg  5258  cbvmptv  5261  mptv  5264  csbmpt12  5557  dfid4  5575  fconstmpt  5737  mptrel  5824  rnmpt  5953  resmpt  6036  mptresid  6049  mptcnv  6137  mptpreima  6235  funmpt  6584  dfmpt3  6682  mptfnf  6683  mptfng  6687  mptun  6694  dffn5  6948  feqmptdf  6960  fvmptg  6994  fvmptndm  7026  fndmin  7044  f1ompt  7108  fmptco  7124  fmptsng  7163  fmptsnd  7164  mpomptx  7518  f1ocnvd  7654  dftpos4  8227  mpocurryd  8251  mapsncnv  8884  marypha2lem3  9429  cardf2  9935  aceq3lem  10112  compsscnv  10363  pjfval2  21256  2ndcdisj  22952  xkocnv  23310  abrexexd  31734  f1o3d  31839  fmptcof2  31870  mptssALT  31888  mpomptxf  31893  f1od2  31934  qqhval2  32951  dfbigcup2  34860  gg-dvcnp2  35163  gg-dvmulbr  35164  gg-dvcobr  35165  gg-cmvth  35170  gg-dvfsumle  35171  gg-dvfsumlem2  35172  bj-0nelmpt  35986  bj-mpomptALT  35989  rnmptsn  36205  curf  36455  curunc  36459  phpreu  36461  poimirlem26  36503  mbfposadd  36524  fnopabco  36580  mptbi12f  37023  fgraphopab  41938  mptssid  43930  dfafn5a  45855  mpomptx2  46964