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 1567	. . . . 5 class 𝑥
6	5, 2	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1567	. . . . 5 class 𝑦
9	8, 3	wceq 1568	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5172	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1568	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  5542  dfid4  5557  fconstmpt  5723  mptrel  5812  rnmpt  5947  resmpt  6039  mptresid  6053  mptcnv  6138  mptpreima  6239  funmpt  6574  dfmpt3  6669  mptfnf  6670  mptfng  6674  mptun  6681  dffn5  6939  feqmptdf  6951  fvmptg  6987  fvmptndm  7021  fndmin  7040  f1ompt  7106  fmptco  7125  fmptsng  7166  fmptsnd  7167  mpomptx  7523  f1ocnvd  7661  dftpos4  8240  mpocurryd  8264  mapsncnv  8890  marypha2lem3  9396  cardf2  9928  aceq3lem  10103  compsscnv  10354  pjfval2  21838  2ndcdisj  23592  xkocnv  23950  dvcnp2  26058  dvmulbr  26077  dvcobr  26084  cmvth  26129  dvfsumle  26159  dvfsumlem2  26165  taylthlem2  26513  abrexexd  32821  f1o3d  32937  fmptcof2  32968  mptssALT  32985  mpomptxf  32989  f1od2  33030  qqhval2  34338  dfbigcup2  36343  cbvmptvw2  36690  cbvmptdavw  36723  cbvmptdavw2  36744  bj-0nelmpt  37702  bj-mpomptALT  37705  rnmptsn  37925  curf  38193  curunc  38197  phpreu  38199  poimirlem26  38241  mbfposadd  38262  fnopabco  38318  mptbi12f  38761  dfqmap3  39043  blockadjliftmap  39053  fgraphopab  43878  mptssid  45904  lambert0  47569  lamberte  47570  sinnpoly  47573  dfafn5a  47842  mpomptx2  49060