Definition df-mpt 4081

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

This definition is referenced by:  mpteq12f  4098  nfmpt  4110  nfmpt1  4111  cbvmptf  4112  cbvmpt  4113  mptv  4115  fconstmpt  4691  mptrel  4773  rnmpt  4893  resmpt  4973  mptresid  4979  mptcnv  5049  mptpreima  5140  funmpt  5273  dfmpt3  5357  mptfng  5360  mptun  5366  dffn5im  5581  fvmptss2  5611  fvmptg  5612  fndmin  5643  f1ompt  5687  fmptco  5702  mpomptx  5986  f1ocnvd  6095  f1od2  6259  dftpos4  6287  mapsncnv  6720