Definition df-mpt 5147

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 5146	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1536	. . . . 5 class 𝑥
6	5, 2	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1536	. . . . 5 class 𝑦
9	8, 3	wceq 1537	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5128	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1537	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12df  5148  mpteq12f  5149  nfmpt  5163  nfmpt1  5164  cbvmptf  5165  cbvmptfg  5166  mptv  5171  csbmpt12  5444  dfid4  5461  fconstmpt  5614  mptrel  5697  rnmpt  5827  resmpt  5905  mptresid  5918  mptresidOLD  5920  mptcnv  5998  mptpreima  6092  funmpt  6393  dfmpt3  6482  mptfnf  6483  mptfng  6487  mptun  6494  dffn5  6724  feqmptdf  6735  fvmptg  6766  fvmptndm  6798  fndmin  6815  f1ompt  6875  fmptco  6891  fmptsng  6930  fmptsnd  6931  mpomptx  7265  f1ocnvd  7396  dftpos4  7911  mpocurryd  7935  mapsncnv  8457  marypha2lem3  8901  cardf2  9372  aceq3lem  9546  compsscnv  9793  pjfval2  20853  2ndcdisj  22064  xkocnv  22422  abrexexd  30269  f1o3d  30372  fmptcof2  30402  mptssALT  30420  mpomptxf  30425  f1od2  30457  qqhval2  31223  dfbigcup2  33360  bj-0nelmpt  34411  bj-mpomptALT  34414  rnmptsn  34619  curf  34885  curunc  34889  phpreu  34891  poimirlem26  34933  mbfposadd  34954  fnopabco  35013  mptbi12f  35459  fgraphopab  39830  mptssid  41531  dfafn5a  43379  mpomptx2  44403