Definition df-mpt 4178

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

This definition is referenced by:  mpteq12f  4195  nfmpt  4207  nfmpt1  4208  cbvmptf  4209  cbvmpt  4210  mptv  4212  fconstmpt  4802  mptrel  4888  rnmpt  5010  resmpt  5091  mptresid  5097  mptcnv  5170  mptpreima  5261  funmpt  5395  dfmpt3  5486  mptfng  5489  mptun  5495  dffn5im  5727  fvmptss2  5757  fvmptg  5758  fndmin  5790  f1ompt  5833  fmptco  5848  mpomptx  6152  f1ocnvd  6265  f1o3d  6271  f1od2  6444  dftpos4  6507  mapsncnv  6943