Definition df-mpt 4152

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

This definition is referenced by:  mpteq12f  4169  nfmpt  4181  nfmpt1  4182  cbvmptf  4183  cbvmpt  4184  mptv  4186  fconstmpt  4773  mptrel  4858  rnmpt  4980  resmpt  5061  mptresid  5067  mptcnv  5139  mptpreima  5230  funmpt  5364  dfmpt3  5455  mptfng  5458  mptun  5464  dffn5im  5691  fvmptss2  5721  fvmptg  5722  fndmin  5754  f1ompt  5798  fmptco  5813  mpomptx  6111  f1ocnvd  6224  f1od2  6399  dftpos4  6428  mapsncnv  6863