Definition df-mpt 5190

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 5189	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1569	. . . . 5 class 𝑥
6	5, 2	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1569	. . . . 5 class 𝑦
9	8, 3	wceq 1570	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5170	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1570	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12da  5191  mpteq12f  5193  mpteq12dva  5194  nfmpt  5206  nfmpt1  5207  cbvmptf  5208  cbvmptfg  5209  cbvmptv  5212  mptv  5214  csbmpt12  5536  dfid4  5551  fconstmpt  5717  mptrel  5808  rnmpt  5945  resmpt  6040  mptresid  6054  mptcnv  6143  mptpreima  6251  funmpt  6595  dfmpt3  6692  mptfnf  6693  mptfng  6697  mptun  6704  dffn5  6963  feqmptdf  6975  fvmptg  7011  fvmptndm  7045  fndmin  7064  f1ompt  7132  fmptco  7151  fmptsng  7193  fmptsnd  7194  mpomptx  7553  f1ocnvd  7693  mpt3mpt  7706  f1od2  8132  dftpos4  8287  mpocurryd  8311  curf  8915  mapsncnv  8946  marypha2lem3  9453  cardf2  10048  aceq3lem  10223  compsscnv  10473  pjfval2  22042  2ndcdisj  23802  xkocnv  24160  dvcnp2  26267  dvmulbr  26286  dvcobr  26293  cmvth  26338  dvfsumle  26368  dvfsumlem2  26374  taylthlem2  26728  abrexexd  33174  f1o3d  33289  fmptcof2  33320  mptssALT  33336  mpomptxf  33340  qqhval2  34681  dfk12  36011  dfk22  36012  dfk32  36013  dfbigcup2  36838  cbvmptvw2  37200  cbvmptdavw  37233  cbvmptdavw2  37254  bj-0nelmpt  38228  bj-mpomptALT  38231  rnmptsn  38449  curunc  38716  phpreu  38718  poimirlem26  38755  mbfposadd  38776  fnopabco  38848  mptbi12f  39289  dfqmap3  39571  blockadjliftmap  39581  fgraphopab  44395  mptssid  46456  lambert0  48140  lamberte  48141  sinnpoly  48144  dfafn5a  48433  mpomptx2  49650