Definition df-mpt 5168

Description: Define maps-to notation for defining a function via a rule. Read as "the function which maps 𝑥 (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 5167	. 2 class (𝑥 ∈ 𝐴 ↦ 𝐵)
5	1	cv 1541	. . . . 5 class 𝑥
6	5, 2	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1541	. . . . 5 class 𝑦
9	8, 3	wceq 1542	. . . 4 wff 𝑦 = 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)
11	10, 1, 7	copab 5148	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
12	4, 11	wceq 1542	1 wff (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}

This definition is referenced by:  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  nfmpt  5184  nfmpt1  5185  cbvmptf  5186  cbvmptfg  5187  cbvmptv  5190  mptv  5192  csbmpt12  5509  dfid4  5524  fconstmpt  5690  mptrel  5778  rnmpt  5910  resmpt  6000  mptresid  6014  mptcnv  6100  mptpreima  6200  funmpt  6534  dfmpt3  6630  mptfnf  6631  mptfng  6635  mptun  6642  dffn5  6896  feqmptdf  6908  fvmptg  6943  fvmptndm  6977  fndmin  6995  f1ompt  7061  fmptco  7080  fmptsng  7120  fmptsnd  7121  mpomptx  7477  f1ocnvd  7615  dftpos4  8192  mpocurryd  8216  mapsncnv  8838  marypha2lem3  9347  cardf2  9864  aceq3lem  10039  compsscnv  10290  pjfval2  21686  2ndcdisj  23418  xkocnv  23776  dvcnp2  25884  dvmulbr  25903  dvcobr  25910  cmvth  25955  dvfsumle  25985  dvfsumlem2  25991  taylthlem2  26336  abrexexd  32576  f1o3d  32696  fmptcof2  32727  mptssALT  32744  mpomptxf  32748  f1od2  32789  qqhval2  34123  dfbigcup2  36076  cbvmptvw2  36413  cbvmptdavw  36446  cbvmptdavw2  36467  bj-0nelmpt  37425  bj-mpomptALT  37428  rnmptsn  37648  curf  37916  curunc  37920  phpreu  37922  poimirlem26  37964  mbfposadd  37985  fnopabco  38041  mptbi12f  38484  dfqmap3  38766  blockadjliftmap  38776  fgraphopab  43628  mptssid  45667  lambert0  47326  lamberte  47327  sinnpoly  47330  dfafn5a  47599  mpomptx2  48802