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  31777  f1o3d  31882  fmptcof2  31913  mptssALT  31931  mpomptxf  31936  f1od2  31977  qqhval2  32993  dfbigcup2  34902  gg-dvcnp2  35205  gg-dvmulbr  35206  gg-dvcobr  35207  gg-cmvth  35212  gg-dvfsumle  35213  gg-dvfsumlem2  35214  bj-0nelmpt  36045  bj-mpomptALT  36048  rnmptsn  36264  curf  36514  curunc  36518  phpreu  36520  poimirlem26  36562  mbfposadd  36583  fnopabco  36639  mptbi12f  37082  fgraphopab  42000  mptssid  43992  dfafn5a  45916  mpomptx2  47058