Definition df-mpt 4763

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 4762	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1522	. . . . 5 class 𝑥
6	5, 2	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1522	. . . . 5 class 𝑦
9	8, 3	wceq 1523	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4745	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1523	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4764  mpteq12d  4767  mpteq12df  4768  nfmpt  4779  nfmpt1  4780  cbvmptf  4781  cbvmpt  4782  mptv  4784  csbmpt12  5039  dfid4  5055  fconstmpt  5197  mptrel  5281  rnmpt  5403  resmpt  5484  mptresid  5491  mptcnv  5569  mptpreima  5666  funmpt  5964  dfmpt3  6052  mptfnf  6053  mptfng  6057  mptun  6063  dffn5  6280  feqmptdf  6290  fvmptg  6319  fvmptndm  6347  fndmin  6364  f1ompt  6422  fmptco  6436  fmptsng  6475  fmptsnd  6476  mpt2mptx  6793  f1ocnvd  6926  dftpos4  7416  mpt2curryd  7440  mapsncnv  7946  marypha2lem3  8384  cardf2  8807  aceq3lem  8981  compsscnv  9231  pjfval2  20101  2ndcdisj  21307  xkocnv  21665  abrexexd  29473  f1o3d  29559  fmptcof2  29585  mptssALT  29602  mpt2mptxf  29605  f1od2  29627  qqhval2  30154  dfbigcup2  32131  bj-0nelmpt  33194  bj-mpt2mptALT  33197  rnmptsn  33312  curf  33517  curunc  33521  phpreu  33523  poimirlem26  33565  mbfposadd  33587  fnopabco  33647  mptbi12f  34105  fgraphopab  38105  mptssid  39764  dfafn5a  41561  mpt2mptx2  42438