Definition df-mpt 4685

Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (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 4683	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1479	. . . . 5 class 𝑥
6	5, 2	wcel 1987	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1479	. . . . 5 class 𝑦
9	8, 3	wceq 1480	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4682	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1480	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4701  mpteq12d  4704  mpteq12df  4705  nfmpt  4716  nfmpt1  4717  cbvmptf  4718  cbvmpt  4719  mptv  4721  csbmpt12  4980  dfid4  5001  fconstmpt  5133  mptrel  5218  rnmpt  5341  resmpt  5418  mptresid  5425  mptcnv  5503  mptpreima  5597  funmpt  5894  dfmpt3  5981  mptfnf  5982  mptfng  5986  mptun  5992  dffn5  6208  feqmptdf  6218  fvmptg  6247  fvmptndm  6274  fndmin  6290  f1ompt  6348  fmptco  6362  fmptsng  6399  fmptsnd  6400  mpt2mptx  6716  f1ocnvd  6849  dftpos4  7331  mpt2curryd  7355  mapsncnv  7864  marypha2lem3  8303  cardf2  8729  aceq3lem  8903  compsscnv  9153  pjfval2  19993  2ndcdisj  21199  xkocnv  21557  abrexexd  29235  f1o3d  29316  fmptcof2  29340  mptssALT  29358  mpt2mptxf  29361  f1od2  29383  qqhval2  29850  dfbigcup2  31701  bj-0nelmpt  32745  bj-mpt2mptALT  32748  rnmptsn  32853  curf  33058  curunc  33062  phpreu  33064  poimirlem26  33106  mbfposadd  33128  fnopabco  33188  mptbi12f  33646  fgraphopab  37308  mptssid  38960  dfafn5a  40574  mpt2mptx2  41431