Definition df-mpt 3991

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 3989	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1330	. . . . 5 class 𝑥
6	5, 2	wcel 1480	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1330	. . . . 5 class 𝑦
9	8, 3	wceq 1331	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 3988	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1331	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4008  nfmpt  4020  nfmpt1  4021  cbvmptf  4022  cbvmpt  4023  mptv  4025  fconstmpt  4586  mptrel  4667  rnmpt  4787  resmpt  4867  mptresid  4873  mptcnv  4941  mptpreima  5032  funmpt  5161  dfmpt3  5245  mptfng  5248  mptun  5254  dffn5im  5467  fvmptss2  5496  fvmptg  5497  fndmin  5527  f1ompt  5571  fmptco  5586  mpomptx  5862  f1ocnvd  5972  f1od2  6132  dftpos4  6160  mapsncnv  6589