Definition df-mpt 4097

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

This definition is referenced by:  mpteq12f  4114  nfmpt  4126  nfmpt1  4127  cbvmptf  4128  cbvmpt  4129  mptv  4131  fconstmpt  4711  mptrel  4795  rnmpt  4915  resmpt  4995  mptresid  5001  mptcnv  5073  mptpreima  5164  funmpt  5297  dfmpt3  5383  mptfng  5386  mptun  5392  dffn5im  5609  fvmptss2  5639  fvmptg  5640  fndmin  5672  f1ompt  5716  fmptco  5731  mpomptx  6017  f1ocnvd  6129  f1od2  6302  dftpos4  6330  mapsncnv  6763