Definition df-mpt 4066

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

This definition is referenced by:  mpteq12f  4083  nfmpt  4095  nfmpt1  4096  cbvmptf  4097  cbvmpt  4098  mptv  4100  fconstmpt  4673  mptrel  4755  rnmpt  4875  resmpt  4955  mptresid  4961  mptcnv  5031  mptpreima  5122  funmpt  5254  dfmpt3  5338  mptfng  5341  mptun  5347  dffn5im  5561  fvmptss2  5591  fvmptg  5592  fndmin  5623  f1ompt  5667  fmptco  5682  mpomptx  5965  f1ocnvd  6072  f1od2  6235  dftpos4  6263  mapsncnv  6694