Definition df-mpt 4874

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 𝑥. An example is the square function for complex numbers, (𝑥 ∈ ℂ ↦ (𝑥↑2)). 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 4873	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1623	. . . . 5 class 𝑥
6	5, 2	wcel 2131	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1623	. . . . 5 class 𝑦
9	8, 3	wceq 1624	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4856	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1624	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4875  mpteq12d  4878  mpteq12df  4879  nfmpt  4890  nfmpt1  4891  cbvmptf  4892  cbvmpt  4893  mptv  4895  csbmpt12  5152  dfid4  5168  fconstmpt  5312  mptrel  5396  rnmpt  5518  resmpt  5599  mptresid  5606  mptcnv  5684  mptpreima  5781  funmpt  6079  dfmpt3  6167  mptfnf  6168  mptfng  6172  mptun  6178  dffn5  6395  feqmptdf  6405  fvmptg  6434  fvmptndm  6462  fndmin  6479  f1ompt  6537  fmptco  6551  fmptsng  6590  fmptsnd  6591  mpt2mptx  6908  f1ocnvd  7041  dftpos4  7532  mpt2curryd  7556  mapsncnv  8062  marypha2lem3  8500  cardf2  8951  aceq3lem  9125  compsscnv  9377  pjfval2  20247  2ndcdisj  21453  xkocnv  21811  abrexexd  29646  f1o3d  29732  fmptcof2  29758  mptssALT  29775  mpt2mptxf  29778  f1od2  29800  qqhval2  30327  dfbigcup2  32304  bj-0nelmpt  33367  bj-mpt2mptALT  33370  rnmptsn  33485  curf  33692  curunc  33696  phpreu  33698  poimirlem26  33740  mbfposadd  33762  fnopabco  33822  mptbi12f  34280  fgraphopab  38282  mptssid  39941  dfafn5a  41738  mpt2mptx2  42615