Definition df-mpt 4147

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 4145	. 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 4144	. 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  4164  nfmpt  4176  nfmpt1  4177  cbvmptf  4178  cbvmpt  4179  mptv  4181  fconstmpt  4768  mptrel  4853  rnmpt  4975  resmpt  5056  mptresid  5062  mptcnv  5134  mptpreima  5225  funmpt  5359  dfmpt3  5449  mptfng  5452  mptun  5458  dffn5im  5684  fvmptss2  5714  fvmptg  5715  fndmin  5747  f1ompt  5791  fmptco  5806  mpomptx  6104  f1ocnvd  6217  f1od2  6392  dftpos4  6420  mapsncnv  6855