Definition df-mpt 4147

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

This definition is referenced by:  mpteq12f  4164  nfmpt  4176  nfmpt1  4177  cbvmptf  4178  cbvmpt  4179  mptv  4181  fconstmpt  4766  mptrel  4850  rnmpt  4972  resmpt  5053  mptresid  5059  mptcnv  5131  mptpreima  5222  funmpt  5356  dfmpt3  5446  mptfng  5449  mptun  5455  dffn5im  5681  fvmptss2  5711  fvmptg  5712  fndmin  5744  f1ompt  5788  fmptco  5803  mpomptx  6101  f1ocnvd  6214  f1od2  6387  dftpos4  6415  mapsncnv  6850