Definition df-mpt 4052

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 4050	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1347	. . . . 5 class 𝑥
6	5, 2	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1347	. . . . 5 class 𝑦
9	8, 3	wceq 1348	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4049	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1348	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4069  nfmpt  4081  nfmpt1  4082  cbvmptf  4083  cbvmpt  4084  mptv  4086  fconstmpt  4658  mptrel  4739  rnmpt  4859  resmpt  4939  mptresid  4945  mptcnv  5013  mptpreima  5104  funmpt  5236  dfmpt3  5320  mptfng  5323  mptun  5329  dffn5im  5542  fvmptss2  5571  fvmptg  5572  fndmin  5603  f1ompt  5647  fmptco  5662  mpomptx  5944  f1ocnvd  6051  f1od2  6214  dftpos4  6242  mapsncnv  6673