Definition df-mpt 4192

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

This definition is referenced by:  mpteq12f  4209  nfmpt  4221  nfmpt1  4222  cbvmptf  4223  cbvmpt  4224  mptv  4226  fconstmpt  4820  mptrel  4906  rnmpt  5028  resmpt  5109  mptresid  5115  mptcnv  5188  mptpreima  5279  funmpt  5413  dfmpt3  5504  mptfng  5507  mptun  5513  dffn5im  5745  fvmptss2  5777  fvmptg  5778  fndmin  5810  f1ompt  5853  fmptco  5868  mpomptx  6172  f1ocnvd  6285  f1o3d  6291  f1od2  6464  dftpos4  6527  mapsncnv  6970