Definition df-mpt 4150

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 4148	. 2 class ( x e. A |-> B )
5	1	cv 1394	. . . . 5 class x
6	5, 2	wcel 2200	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1394	. . . . 5 class y
9	8, 3	wceq 1395	. . . 4 wff y = B
10	6, 9	wa 104	. . 3 wff ( x e. A /\ y = B )
11	10, 1, 7	copab 4147	. 2 class { <. x , y >. | ( x e. A /\ y = B ) }
12	4, 11	wceq 1395	1 wff ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

This definition is referenced by:  mpteq12f  4167  nfmpt  4179  nfmpt1  4180  cbvmptf  4181  cbvmpt  4182  mptv  4184  fconstmpt  4771  mptrel  4856  rnmpt  4978  resmpt  5059  mptresid  5065  mptcnv  5137  mptpreima  5228  funmpt  5362  dfmpt3  5452  mptfng  5455  mptun  5461  dffn5im  5687  fvmptss2  5717  fvmptg  5718  fndmin  5750  f1ompt  5794  fmptco  5809  mpomptx  6107  f1ocnvd  6220  f1od2  6395  dftpos4  6424  mapsncnv  6859