Definition df-mpt 4067

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 4065	. 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 4064	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1353	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4084  nfmpt  4096  nfmpt1  4097  cbvmptf  4098  cbvmpt  4099  mptv  4101  fconstmpt  4674  mptrel  4756  rnmpt  4876  resmpt  4956  mptresid  4962  mptcnv  5032  mptpreima  5123  funmpt  5255  dfmpt3  5339  mptfng  5342  mptun  5348  dffn5im  5562  fvmptss2  5592  fvmptg  5593  fndmin  5624  f1ompt  5668  fmptco  5683  mpomptx  5966  f1ocnvd  6073  f1od2  6236  dftpos4  6264  mapsncnv  6695