Definition df-mpt 5233

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

This definition is referenced by:  mpteq12da  5234  mpteq12dfOLD  5236  mpteq12f  5237  mpteq12dva  5238  nfmpt  5256  nfmpt1  5257  cbvmptf  5258  cbvmptfg  5259  cbvmptv  5262  mptv  5265  csbmpt12  5558  dfid4  5576  fconstmpt  5739  mptrel  5826  rnmpt  5955  resmpt  6038  mptresid  6051  mptcnv  6140  mptpreima  6238  funmpt  6587  dfmpt3  6685  mptfnf  6686  mptfng  6690  mptun  6697  dffn5  6951  feqmptdf  6963  fvmptg  6997  fvmptndm  7029  fndmin  7047  f1ompt  7111  fmptco  7127  fmptsng  7166  fmptsnd  7167  mpomptx  7521  f1ocnvd  7657  dftpos4  8230  mpocurryd  8254  mapsncnv  8887  marypha2lem3  9432  cardf2  9938  aceq3lem  10115  compsscnv  10366  pjfval2  21264  2ndcdisj  22960  xkocnv  23318  abrexexd  31746  f1o3d  31851  fmptcof2  31882  mptssALT  31900  mpomptxf  31905  f1od2  31946  qqhval2  32962  dfbigcup2  34871  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  bj-0nelmpt  35997  bj-mpomptALT  36000  rnmptsn  36216  curf  36466  curunc  36470  phpreu  36472  poimirlem26  36514  mbfposadd  36535  fnopabco  36591  mptbi12f  37034  fgraphopab  41952  mptssid  43944  dfafn5a  45868  mpomptx2  47010