Definition df-mpt 5159

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

This definition is referenced by:  mpteq12da  5160  mpteq12dfOLD  5162  mpteq12f  5163  mpteq12dva  5164  nfmpt  5182  nfmpt1  5183  cbvmptf  5184  cbvmptfg  5185  cbvmptv  5188  mptv  5191  csbmpt12  5471  dfid4  5491  fconstmpt  5650  mptrel  5737  rnmpt  5867  resmpt  5948  mptresid  5961  mptresidOLD  5963  mptcnv  6048  mptpreima  6146  funmpt  6479  dfmpt3  6576  mptfnf  6577  mptfng  6581  mptun  6588  dffn5  6837  feqmptdf  6848  fvmptg  6882  fvmptndm  6914  fndmin  6931  f1ompt  6994  fmptco  7010  fmptsng  7049  fmptsnd  7050  mpomptx  7396  f1ocnvd  7529  dftpos4  8070  mpocurryd  8094  mapsncnv  8690  marypha2lem3  9205  cardf2  9710  aceq3lem  9885  compsscnv  10136  pjfval2  20925  2ndcdisj  22616  xkocnv  22974  abrexexd  30863  f1o3d  30971  fmptcof2  31003  mptssALT  31021  mpomptxf  31025  f1od2  31065  qqhval2  31941  dfbigcup2  34210  bj-0nelmpt  35296  bj-mpomptALT  35299  rnmptsn  35515  curf  35764  curunc  35768  phpreu  35770  poimirlem26  35812  mbfposadd  35833  fnopabco  35890  mptbi12f  36333  fgraphopab  41042  mptssid  42792  dfafn5a  44663  mpomptx2  45681