Definition df-mpt 4096

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

This definition is referenced by:  mpteq12f  4113  nfmpt  4125  nfmpt1  4126  cbvmptf  4127  cbvmpt  4128  mptv  4130  fconstmpt  4710  mptrel  4794  rnmpt  4914  resmpt  4994  mptresid  5000  mptcnv  5072  mptpreima  5163  funmpt  5296  dfmpt3  5380  mptfng  5383  mptun  5389  dffn5im  5606  fvmptss2  5636  fvmptg  5637  fndmin  5669  f1ompt  5713  fmptco  5728  mpomptx  6013  f1ocnvd  6125  f1od2  6293  dftpos4  6321  mapsncnv  6754