Definition df-mpt 3999

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

This definition is referenced by:  mpteq12f  4016  nfmpt  4028  nfmpt1  4029  cbvmptf  4030  cbvmpt  4031  mptv  4033  fconstmpt  4594  mptrel  4675  rnmpt  4795  resmpt  4875  mptresid  4881  mptcnv  4949  mptpreima  5040  funmpt  5169  dfmpt3  5253  mptfng  5256  mptun  5262  dffn5im  5475  fvmptss2  5504  fvmptg  5505  fndmin  5535  f1ompt  5579  fmptco  5594  mpomptx  5870  f1ocnvd  5980  f1od2  6140  dftpos4  6168  mapsncnv  6597