Definition df-mpt 4111

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

This definition is referenced by:  mpteq12f  4128  nfmpt  4140  nfmpt1  4141  cbvmptf  4142  cbvmpt  4143  mptv  4145  fconstmpt  4726  mptrel  4810  rnmpt  4931  resmpt  5012  mptresid  5018  mptcnv  5090  mptpreima  5181  funmpt  5314  dfmpt3  5404  mptfng  5407  mptun  5413  dffn5im  5631  fvmptss2  5661  fvmptg  5662  fndmin  5694  f1ompt  5738  fmptco  5753  mpomptx  6043  f1ocnvd  6155  f1od2  6328  dftpos4  6356  mapsncnv  6789