Definition df-mpt 4639

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 4637	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1473	. . . . 5 class 𝑥
6	5, 2	wcel 1976	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1473	. . . . 5 class 𝑦
9	8, 3	wceq 1474	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 382	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 4636	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1474	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12f  4655  nfmpt  4668  nfmpt1  4669  cbvmptf  4670  cbvmpt  4671  mptv  4673  csbmpt12  4923  dfid4  4944  fconstmpt  5074  mptrel  5157  rnmpt  5278  resmpt  5355  mptresid  5361  mptcnv  5439  mptpreima  5530  funmpt  5825  dfmpt3  5912  mptfnf  5913  mptfng  5917  mptun  5923  dffn5  6135  feqmptdf  6145  fvmptg  6173  fvmptndm  6200  fndmin  6216  f1ompt  6274  fmptco  6287  fmptsng  6316  fmptsnd  6317  mpt2mptx  6626  f1ocnvd  6759  dftpos4  7235  mpt2curryd  7259  mapsncnv  7767  marypha2lem3  8203  cardf2  8629  aceq3lem  8803  compsscnv  9053  pjfval2  19819  2ndcdisj  21016  xkocnv  21374  clwwlknprop  26093  abrexexd  28524  f1o3d  28606  mpteq12df  28630  fmptcof2  28632  mptssALT  28650  mpt2mptxf  28653  f1od2  28680  qqhval2  29147  mpteq12d  30708  dfbigcup2  30969  bj-0nelmpt  32033  bj-mpt2mptALT  32036  rnmptsn  32141  curf  32340  curunc  32344  phpreu  32346  poimirlem26  32388  mbfposadd  32410  fnopabco  32470  mptbi12f  32928  fgraphopab  36590  dfafn5a  39673  mpt2mptx2  41887