Definition df-mpt 4195

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 4193	. 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 4192	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1402	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is used by:  mpteq12f  4212  nfmpt  4225  nfmpt1  4226  cbvmptf  4227  cbvmpt  4228  mptv  4230  fconstmpt  4824  mptrel  4910  rnmpt  5032  resmpt  5114  mptresid  5120  mptcnv  5193  mptpreima  5284  funmpt  5418  dfmpt3  5509  mptfng  5512  mptun  5518  dffn5im  5751  fvmptss2  5783  fvmptg  5784  fvmptndm  5807  fndmin  5819  f1ompt  5862  fmptco  5877  mptmex  5948  mpomptx  6182  f1ocnvd  6295  f1o3d  6301  f1od2  6475  dftpos4  6538  mapsncnv  6981