Definition df-mpt 4126

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

This definition is referenced by:  mpteq12f  4143  nfmpt  4155  nfmpt1  4156  cbvmptf  4157  cbvmpt  4158  mptv  4160  fconstmpt  4743  mptrel  4827  rnmpt  4948  resmpt  5029  mptresid  5035  mptcnv  5107  mptpreima  5198  funmpt  5332  dfmpt3  5422  mptfng  5425  mptun  5431  dffn5im  5652  fvmptss2  5682  fvmptg  5683  fndmin  5715  f1ompt  5759  fmptco  5774  mpomptx  6066  f1ocnvd  6178  f1od2  6351  dftpos4  6379  mapsncnv  6812