Definition df-mpt 5003

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 5002	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1506	. . . . 5 class 𝑥
6	5, 2	wcel 2048	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1506	. . . . 5 class 𝑦
9	8, 3	wceq 1507	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 387	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4985	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1507	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  5004  mpteq12df  5007  nfmpt  5018  nfmpt1  5019  cbvmptf  5020  cbvmpt  5021  mptv  5023  csbmpt12  5289  dfid4  5307  fconstmpt  5457  mptrel  5540  rnmpt  5663  resmpt  5744  mptresid  5756  mptcnv  5832  mptpreima  5925  funmpt  6220  dfmpt3  6306  mptfnf  6307  mptfng  6311  mptun  6318  dffn5  6548  feqmptdf  6558  fvmptg  6587  fvmptndm  6617  fndmin  6634  f1ompt  6692  fmptco  6708  fmptsng  6747  fmptsnd  6748  mpomptx  7075  f1ocnvd  7208  dftpos4  7707  mpocurryd  7731  mapsncnv  8247  marypha2lem3  8688  cardf2  9158  aceq3lem  9332  compsscnv  9583  pjfval2  20545  2ndcdisj  21758  xkocnv  22116  abrexexd  30038  f1o3d  30126  fmptcof2  30154  mptssALT  30172  mpomptxf  30175  f1od2  30198  qqhval2  30824  dfbigcup2  32821  bj-0nelmpt  33852  bj-mpomptALT  33855  rnmptsn  33993  curf  34259  curunc  34263  phpreu  34265  poimirlem26  34307  mbfposadd  34328  fnopabco  34388  mptbi12f  34836  fgraphopab  39151  mptssid  40884  dfafn5a  42711  mpt2mptx2  43687