Definition df-mpt 4157

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 𝑥. 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 4155	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1397	. . . . 5 class 𝑥
6	5, 2	wcel 2202	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1397	. . . . 5 class 𝑦
9	8, 3	wceq 1398	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4154	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1398	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4174  nfmpt  4186  nfmpt1  4187  cbvmptf  4188  cbvmpt  4189  mptv  4191  fconstmpt  4779  mptrel  4864  rnmpt  4986  resmpt  5067  mptresid  5073  mptcnv  5146  mptpreima  5237  funmpt  5371  dfmpt3  5462  mptfng  5465  mptun  5471  dffn5im  5700  fvmptss2  5730  fvmptg  5731  fndmin  5763  f1ompt  5806  fmptco  5821  mpomptx  6122  f1ocnvd  6235  f1od2  6409  dftpos4  6472  mapsncnv  6907