Definition df-mpt 3841

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 3839	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1283	. . . . 5 class 𝑥
6	5, 2	wcel 1433	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1283	. . . . 5 class 𝑦
9	8, 3	wceq 1284	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 3838	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1284	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  3858  nfmpt  3870  nfmpt1  3871  cbvmpt  3872  mptv  3874  fconstmpt  4405  rnmpt  4600  resmpt  4676  mptresid  4680  mptpreima  4834  funmpt  4958  dfmpt3  5041  mptfng  5044  mptun  5049  dffn5im  5240  fvmptss2  5268  fvmptg  5269  fndmin  5295  f1ompt  5341  fmptco  5351  mpt2mptx  5615  f1ocnvd  5722  f1od2  5876  dftpos4  5901