Definition df-mpt 5237

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 5236	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1533	. . . . 5 class 𝑥
6	5, 2	wcel 2099	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1533	. . . . 5 class 𝑦
9	8, 3	wceq 1534	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5215	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1534	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5238  mpteq12dfOLD  5240  mpteq12f  5241  mpteq12dva  5242  nfmpt  5260  nfmpt1  5261  cbvmptf  5262  cbvmptfg  5263  cbvmptv  5266  mptv  5269  csbmpt12  5563  dfid4  5581  fconstmpt  5744  mptrel  5831  rnmpt  5961  resmpt  6046  mptresid  6060  mptcnv  6151  mptpreima  6249  funmpt  6597  dfmpt3  6695  mptfnf  6696  mptfng  6700  mptun  6707  dffn5  6961  feqmptdf  6973  fvmptg  7007  fvmptndm  7040  fndmin  7058  f1ompt  7125  fmptco  7143  fmptsng  7182  fmptsnd  7183  mpomptx  7538  f1ocnvd  7677  dftpos4  8260  mpocurryd  8284  mapsncnv  8922  marypha2lem3  9480  cardf2  9986  aceq3lem  10163  compsscnv  10414  pjfval2  21707  2ndcdisj  23451  xkocnv  23809  dvcnp2  25940  dvmulbr  25960  dvcobr  25968  cmvth  26014  dvfsumle  26045  dvfsumlem2  26052  taylthlem2  26402  abrexexd  32434  f1o3d  32544  fmptcof2  32574  mptssALT  32592  mpomptxf  32595  f1od2  32635  qqhval2  33797  dfbigcup2  35723  bj-0nelmpt  36823  bj-mpomptALT  36826  rnmptsn  37042  curf  37299  curunc  37303  phpreu  37305  poimirlem26  37347  mbfposadd  37368  fnopabco  37424  mptbi12f  37867  fgraphopab  42868  mptssid  44849  dfafn5a  46773  mpomptx2  47713

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »