Definition df-mpt 4044

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

This definition is referenced by:  mpteq12f  4061  nfmpt  4073  nfmpt1  4074  cbvmptf  4075  cbvmpt  4076  mptv  4078  fconstmpt  4650  mptrel  4731  rnmpt  4851  resmpt  4931  mptresid  4937  mptcnv  5005  mptpreima  5096  funmpt  5225  dfmpt3  5309  mptfng  5312  mptun  5318  dffn5im  5531  fvmptss2  5560  fvmptg  5561  fndmin  5591  f1ompt  5635  fmptco  5650  mpomptx  5929  f1ocnvd  6039  f1od2  6199  dftpos4  6227  mapsncnv  6657