Definition df-mpt 5182

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 5181	. 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 5162	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1542	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  nfmpt  5198  nfmpt1  5199  cbvmptf  5200  cbvmptfg  5201  cbvmptv  5204  mptv  5206  csbmpt12  5515  dfid4  5530  fconstmpt  5696  mptrel  5784  rnmpt  5916  resmpt  6006  mptresid  6020  mptcnv  6106  mptpreima  6206  funmpt  6540  dfmpt3  6636  mptfnf  6637  mptfng  6641  mptun  6648  dffn5  6902  feqmptdf  6914  fvmptg  6949  fvmptndm  6983  fndmin  7001  f1ompt  7067  fmptco  7086  fmptsng  7126  fmptsnd  7127  mpomptx  7483  f1ocnvd  7621  dftpos4  8199  mpocurryd  8223  mapsncnv  8845  marypha2lem3  9354  cardf2  9869  aceq3lem  10044  compsscnv  10295  pjfval2  21681  2ndcdisj  23417  xkocnv  23775  dvcnp2  25894  dvmulbr  25914  dvcobr  25922  cmvth  25968  dvfsumle  25999  dvfsumlem2  26006  taylthlem2  26355  abrexexd  32602  f1o3d  32722  fmptcof2  32753  mptssALT  32770  mpomptxf  32774  f1od2  32815  qqhval2  34166  dfbigcup2  36119  cbvmptvw2  36456  cbvmptdavw  36489  cbvmptdavw2  36510  bj-0nelmpt  37396  bj-mpomptALT  37399  rnmptsn  37617  curf  37878  curunc  37882  phpreu  37884  poimirlem26  37926  mbfposadd  37947  fnopabco  38003  mptbi12f  38446  dfqmap3  38728  blockadjliftmap  38738  fgraphopab  43589  mptssid  45628  lambert0  47276  lamberte  47277  sinnpoly  47280  dfafn5a  47549  mpomptx2  48724