Definition df-mpt 4045

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. 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 4043	. 2 class ( x e. A |-> B )
5	1	cv 1342	. . . . 5 class x
6	5, 2	wcel 2136	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1342	. . . . 5 class y
9	8, 3	wceq 1343	. . . 4 wff y = B
10	6, 9	wa 103	. . 3 wff ( x e. A /\ y = B )
11	10, 1, 7	copab 4042	. 2 class { <. x , y >. | ( x e. A /\ y = B ) }
12	4, 11	wceq 1343	1 wff ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

This definition is referenced by:  mpteq12f  4062  nfmpt  4074  nfmpt1  4075  cbvmptf  4076  cbvmpt  4077  mptv  4079  fconstmpt  4651  mptrel  4732  rnmpt  4852  resmpt  4932  mptresid  4938  mptcnv  5006  mptpreima  5097  funmpt  5226  dfmpt3  5310  mptfng  5313  mptun  5319  dffn5im  5532  fvmptss2  5561  fvmptg  5562  fndmin  5592  f1ompt  5636  fmptco  5651  mpomptx  5933  f1ocnvd  6040  f1od2  6203  dftpos4  6231  mapsncnv  6661