Definition df-mpt 5175

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

This definition is referenced by:  mpteq12da  5176  mpteq12f  5178  mpteq12dva  5179  nfmpt  5191  nfmpt1  5192  cbvmptf  5193  cbvmptfg  5194  cbvmptv  5197  mptv  5199  csbmpt12  5500  dfid4  5515  fconstmpt  5681  mptrel  5769  rnmpt  5901  resmpt  5990  mptresid  6004  mptcnv  6090  mptpreima  6190  funmpt  6524  dfmpt3  6620  mptfnf  6621  mptfng  6625  mptun  6632  dffn5  6886  feqmptdf  6898  fvmptg  6933  fvmptndm  6966  fndmin  6984  f1ompt  7050  fmptco  7068  fmptsng  7108  fmptsnd  7109  mpomptx  7465  f1ocnvd  7603  dftpos4  8181  mpocurryd  8205  mapsncnv  8823  marypha2lem3  9328  cardf2  9843  aceq3lem  10018  compsscnv  10269  pjfval2  21648  2ndcdisj  23372  xkocnv  23730  dvcnp2  25849  dvmulbr  25869  dvcobr  25877  cmvth  25923  dvfsumle  25954  dvfsumlem2  25961  taylthlem2  26310  abrexexd  32491  f1o3d  32610  fmptcof2  32641  mptssALT  32659  mpomptxf  32663  f1od2  32706  qqhval2  34016  dfbigcup2  35962  cbvmptvw2  36299  cbvmptdavw  36332  cbvmptdavw2  36353  bj-0nelmpt  37181  bj-mpomptALT  37184  rnmptsn  37400  curf  37658  curunc  37662  phpreu  37664  poimirlem26  37706  mbfposadd  37727  fnopabco  37783  mptbi12f  38226  blockadjliftmap  38492  fgraphopab  43320  mptssid  45362  lambert0  47011  lamberte  47012  sinnpoly  47015  dfafn5a  47284  mpomptx2  48459