Definition df-mpt 3923

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

This definition is referenced by:  mpteq12f  3940  nfmpt  3952  nfmpt1  3953  cbvmptf  3954  cbvmpt  3955  mptv  3957  fconstmpt  4514  mptrel  4595  rnmpt  4715  resmpt  4793  mptresid  4799  mptcnv  4867  mptpreima  4958  funmpt  5086  dfmpt3  5170  mptfng  5173  mptun  5178  dffn5im  5385  fvmptss2  5414  fvmptg  5415  fndmin  5445  f1ompt  5489  fmptco  5503  mpt2mptx  5777  f1ocnvd  5884  f1od2  6038  dftpos4  6066  mapsncnv  6492