Definition df-mpt 3878

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 3876	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1286	. . . . 5 class 𝑥
6	5, 2	wcel 1436	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1286	. . . . 5 class 𝑦
9	8, 3	wceq 1287	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 3875	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1287	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  3895  nfmpt  3907  nfmpt1  3908  cbvmptf  3909  cbvmpt  3910  mptv  3912  fconstmpt  4455  rnmpt  4653  resmpt  4729  mptresid  4735  mptpreima  4892  funmpt  5019  dfmpt3  5103  mptfng  5106  mptun  5111  dffn5im  5315  fvmptss2  5344  fvmptg  5345  fndmin  5371  f1ompt  5415  fmptco  5429  mpt2mptx  5698  f1ocnvd  5805  f1od2  5959  dftpos4  5984  mapsncnv  6406