Definition df-mpt 5192

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

This definition is referenced by:  mpteq12da  5193  mpteq12f  5195  mpteq12dva  5196  nfmpt  5208  nfmpt1  5209  cbvmptf  5210  cbvmptfg  5211  cbvmptv  5214  mptv  5216  csbmpt12  5520  dfid4  5537  fconstmpt  5703  mptrel  5791  rnmpt  5924  resmpt  6011  mptresid  6025  mptcnv  6115  mptpreima  6214  funmpt  6557  dfmpt3  6655  mptfnf  6656  mptfng  6660  mptun  6667  dffn5  6922  feqmptdf  6934  fvmptg  6969  fvmptndm  7002  fndmin  7020  f1ompt  7086  fmptco  7104  fmptsng  7145  fmptsnd  7146  mpomptx  7505  f1ocnvd  7643  dftpos4  8227  mpocurryd  8251  mapsncnv  8869  marypha2lem3  9395  cardf2  9903  aceq3lem  10080  compsscnv  10331  pjfval2  21625  2ndcdisj  23350  xkocnv  23708  dvcnp2  25828  dvmulbr  25848  dvcobr  25856  cmvth  25902  dvfsumle  25933  dvfsumlem2  25940  taylthlem2  26289  abrexexd  32445  f1o3d  32558  fmptcof2  32588  mptssALT  32606  mpomptxf  32608  f1od2  32651  qqhval2  33979  dfbigcup2  35894  cbvmptvw2  36229  cbvmptdavw  36262  cbvmptdavw2  36283  bj-0nelmpt  37111  bj-mpomptALT  37114  rnmptsn  37330  curf  37599  curunc  37603  phpreu  37605  poimirlem26  37647  mbfposadd  37668  fnopabco  37724  mptbi12f  38167  fgraphopab  43199  mptssid  45242  lambert0  46895  lamberte  46896  dfafn5a  47165  mpomptx2  48327