Definition df-mpt 5168

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

This definition is referenced by:  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  nfmpt  5184  nfmpt1  5185  cbvmptf  5186  cbvmptfg  5187  cbvmptv  5190  mptv  5192  csbmpt12  5503  dfid4  5518  fconstmpt  5684  mptrel  5772  rnmpt  5904  resmpt  5994  mptresid  6008  mptcnv  6094  mptpreima  6194  funmpt  6528  dfmpt3  6624  mptfnf  6625  mptfng  6629  mptun  6636  dffn5  6890  feqmptdf  6902  fvmptg  6937  fvmptndm  6971  fndmin  6989  f1ompt  7055  fmptco  7074  fmptsng  7114  fmptsnd  7115  mpomptx  7471  f1ocnvd  7609  dftpos4  8186  mpocurryd  8210  mapsncnv  8832  marypha2lem3  9341  cardf2  9856  aceq3lem  10031  compsscnv  10282  pjfval2  21666  2ndcdisj  23399  xkocnv  23757  dvcnp2  25865  dvmulbr  25884  dvcobr  25891  cmvth  25936  dvfsumle  25967  dvfsumlem2  25974  taylthlem2  26322  abrexexd  32568  f1o3d  32688  fmptcof2  32719  mptssALT  32736  mpomptxf  32740  f1od2  32781  qqhval2  34132  dfbigcup2  36085  cbvmptvw2  36422  cbvmptdavw  36455  cbvmptdavw2  36476  bj-0nelmpt  37426  bj-mpomptALT  37429  rnmptsn  37647  curf  37910  curunc  37914  phpreu  37916  poimirlem26  37958  mbfposadd  37979  fnopabco  38035  mptbi12f  38478  dfqmap3  38760  blockadjliftmap  38770  fgraphopab  43634  mptssid  45673  lambert0  47321  lamberte  47322  sinnpoly  47325  dfafn5a  47594  mpomptx2  48769