Definition df-mpt 5189

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

This definition is referenced by:  mpteq12da  5190  mpteq12f  5192  mpteq12dva  5193  nfmpt  5205  nfmpt1  5206  cbvmptf  5207  cbvmptfg  5208  cbvmptv  5211  mptv  5213  csbmpt12  5517  dfid4  5534  fconstmpt  5700  mptrel  5788  rnmpt  5921  resmpt  6008  mptresid  6022  mptcnv  6112  mptpreima  6211  funmpt  6554  dfmpt3  6652  mptfnf  6653  mptfng  6657  mptun  6664  dffn5  6919  feqmptdf  6931  fvmptg  6966  fvmptndm  6999  fndmin  7017  f1ompt  7083  fmptco  7101  fmptsng  7142  fmptsnd  7143  mpomptx  7502  f1ocnvd  7640  dftpos4  8224  mpocurryd  8248  mapsncnv  8866  marypha2lem3  9388  cardf2  9896  aceq3lem  10073  compsscnv  10324  pjfval2  21618  2ndcdisj  23343  xkocnv  23701  dvcnp2  25821  dvmulbr  25841  dvcobr  25849  cmvth  25895  dvfsumle  25926  dvfsumlem2  25933  taylthlem2  26282  abrexexd  32438  f1o3d  32551  fmptcof2  32581  mptssALT  32599  mpomptxf  32601  f1od2  32644  qqhval2  33972  dfbigcup2  35887  cbvmptvw2  36222  cbvmptdavw  36255  cbvmptdavw2  36276  bj-0nelmpt  37104  bj-mpomptALT  37107  rnmptsn  37323  curf  37592  curunc  37596  phpreu  37598  poimirlem26  37640  mbfposadd  37661  fnopabco  37717  mptbi12f  38160  fgraphopab  43192  mptssid  45235  lambert0  46888  lamberte  46889  sinnpoly  46892  dfafn5a  47161  mpomptx2  48323