Definition df-mpt 4148

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

This definition is referenced by:  mpteq12f  4165  nfmpt  4177  nfmpt1  4178  cbvmptf  4179  cbvmpt  4180  mptv  4182  fconstmpt  4769  mptrel  4854  rnmpt  4976  resmpt  5057  mptresid  5063  mptcnv  5135  mptpreima  5226  funmpt  5360  dfmpt3  5450  mptfng  5453  mptun  5459  dffn5im  5685  fvmptss2  5715  fvmptg  5716  fndmin  5748  f1ompt  5792  fmptco  5807  mpomptx  6105  f1ocnvd  6218  f1od2  6393  dftpos4  6422  mapsncnv  6857