Definition df-mpt 4730

Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B ( x )." The class expression B is the value of the function at x and normally contains the variable x. An example is the square function for complex numbers, ( x e. CC |-> ( x ^ 2 ) ). Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)

Assertion

Ref	Expression
df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

Distinct variable groups:   x, y   y, A   y, B

Allowed substitution hints:   A( x)   B( x)

Detailed syntax breakdown of Definition df-mpt

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cmpt 4729	. 2 class ( x e. A |-> B )
5	1	cv 1482	. . . . 5 class x
6	5, 2	wcel 1990	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1482	. . . . 5 class y
9	8, 3	wceq 1483	. . . 4 wff y = B
10	6, 9	wa 384	. . 3 wff ( x e. A /\ y = B )
11	10, 1, 7	copab 4712	. 2 class { <. x , y >. | ( x e. A /\ y = B ) }
12	4, 11	wceq 1483	1 wff ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

This definition is referenced by:  mpteq12f  4731  mpteq12d  4734  mpteq12df  4735  nfmpt  4746  nfmpt1  4747  cbvmptf  4748  cbvmpt  4749  mptv  4751  csbmpt12  5010  dfid4  5026  fconstmpt  5163  mptrel  5248  rnmpt  5371  resmpt  5449  mptresid  5456  mptcnv  5534  mptpreima  5628  funmpt  5926  dfmpt3  6014  mptfnf  6015  mptfng  6019  mptun  6025  dffn5  6241  feqmptdf  6251  fvmptg  6280  fvmptndm  6308  fndmin  6324  f1ompt  6382  fmptco  6396  fmptsng  6434  fmptsnd  6435  mpt2mptx  6751  f1ocnvd  6884  dftpos4  7371  mpt2curryd  7395  mapsncnv  7904  marypha2lem3  8343  cardf2  8769  aceq3lem  8943  compsscnv  9193  pjfval2  20053  2ndcdisj  21259  xkocnv  21617  abrexexd  29347  f1o3d  29431  fmptcof2  29457  mptssALT  29474  mpt2mptxf  29477  f1od2  29499  qqhval2  30026  dfbigcup2  32006  bj-0nelmpt  33069  bj-mpt2mptALT  33072  rnmptsn  33182  curf  33387  curunc  33391  phpreu  33393  poimirlem26  33435  mbfposadd  33457  fnopabco  33517  mptbi12f  33975  fgraphopab  37788  mptssid  39450  dfafn5a  41240  mpt2mptx2  42113