Definition df-mpt 4175

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

This definition is referenced by:  mpteq12f  4192  nfmpt  4204  nfmpt1  4205  cbvmptf  4206  cbvmpt  4207  mptv  4209  fconstmpt  4799  mptrel  4885  rnmpt  5007  resmpt  5088  mptresid  5094  mptcnv  5167  mptpreima  5258  funmpt  5392  dfmpt3  5483  mptfng  5486  mptun  5492  dffn5im  5724  fvmptss2  5754  fvmptg  5755  fndmin  5787  f1ompt  5830  fmptco  5845  mpomptx  6146  f1ocnvd  6259  f1od2  6433  dftpos4  6496  mapsncnv  6932