Definition df-mpt 5186

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 5185	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1568	. . . . 5 class 𝑥
6	5, 2	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1568	. . . . 5 class 𝑦
9	8, 3	wceq 1569	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1569	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  nfmpt  5202  nfmpt1  5203  cbvmptf  5204  cbvmptfg  5205  cbvmptv  5208  mptv  5210  csbmpt12  5531  dfid4  5546  fconstmpt  5712  mptrel  5802  rnmpt  5938  resmpt  6028  mptresid  6042  mptcnv  6131  mptpreima  6239  funmpt  6578  dfmpt3  6673  mptfnf  6674  mptfng  6678  mptun  6685  dffn5  6943  feqmptdf  6955  fvmptg  6991  fvmptndm  7025  fndmin  7044  f1ompt  7111  fmptco  7130  fmptsng  7173  fmptsnd  7174  mpomptx  7533  f1ocnvd  7672  mpt3mpt  7685  dftpos4  8262  mpocurryd  8286  curf  8890  mapsncnv  8921  marypha2lem3  9429  cardf2  10024  aceq3lem  10199  compsscnv  10449  pjfval2  22015  2ndcdisj  23775  xkocnv  24133  dvcnp2  26240  dvmulbr  26259  dvcobr  26266  cmvth  26311  dvfsumle  26341  dvfsumlem2  26347  taylthlem2  26701  abrexexd  33147  f1o3d  33262  fmptcof2  33293  mptssALT  33310  mpomptxf  33314  f1od2  33353  qqhval2  34656  dfbigcup2  36703  cbvmptvw2  37065  cbvmptdavw  37098  cbvmptdavw2  37119  bj-0nelmpt  38080  bj-mpomptALT  38083  rnmptsn  38301  curunc  38568  phpreu  38570  poimirlem26  38607  mbfposadd  38628  fnopabco  38700  mptbi12f  39141  dfqmap3  39423  blockadjliftmap  39433  fgraphopab  44247  mptssid  46295  lambert0  47979  lamberte  47980  sinnpoly  47983  dfafn5a  48272  mpomptx2  49489