Definition df-mpt 4194

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

This definition is used by:  mpteq12f  4211  nfmpt  4223  nfmpt1  4224  cbvmptf  4225  cbvmpt  4226  mptv  4228  fconstmpt  4822  mptrel  4908  rnmpt  5030  resmpt  5111  mptresid  5117  mptcnv  5190  mptpreima  5281  funmpt  5415  dfmpt3  5506  mptfng  5509  mptun  5515  dffn5im  5748  fvmptss2  5780  fvmptg  5781  fvmptndm  5804  fndmin  5816  f1ompt  5859  fmptco  5874  mptmex  5945  mpomptx  6179  f1ocnvd  6292  f1o3d  6298  f1od2  6471  dftpos4  6534  mapsncnv  6977