Definition df-mpt 5121

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 5120	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1542	. . . . 5 class 𝑥
6	5, 2	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1542	. . . . 5 class 𝑦
9	8, 3	wceq 1543	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5101	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1543	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12df  5122  mpteq12f  5123  nfmpt  5137  nfmpt1  5138  cbvmptf  5139  cbvmptfg  5140  mptv  5145  csbmpt12  5423  dfid4  5441  fconstmpt  5596  mptrel  5680  rnmpt  5809  resmpt  5890  mptresid  5903  mptresidOLD  5905  mptcnv  5983  mptpreima  6081  funmpt  6396  dfmpt3  6490  mptfnf  6491  mptfng  6495  mptun  6502  dffn5  6749  feqmptdf  6760  fvmptg  6794  fvmptndm  6826  fndmin  6843  f1ompt  6906  fmptco  6922  fmptsng  6961  fmptsnd  6962  mpomptx  7301  f1ocnvd  7434  dftpos4  7965  mpocurryd  7989  mapsncnv  8552  marypha2lem3  9031  cardf2  9524  aceq3lem  9699  compsscnv  9950  pjfval2  20625  2ndcdisj  22307  xkocnv  22665  abrexexd  30527  f1o3d  30635  fmptcof2  30668  mptssALT  30686  mpomptxf  30690  f1od2  30730  qqhval2  31598  dfbigcup2  33887  bj-0nelmpt  34971  bj-mpomptALT  34974  rnmptsn  35192  curf  35441  curunc  35445  phpreu  35447  poimirlem26  35489  mbfposadd  35510  fnopabco  35567  mptbi12f  36010  fgraphopab  40679  mptssid  42398  dfafn5a  44267  mpomptx2  45286