Definition df-mpt 4146

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 4144	. 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 4143	. 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  4163  nfmpt  4175  nfmpt1  4176  cbvmptf  4177  cbvmpt  4178  mptv  4180  fconstmpt  4765  mptrel  4849  rnmpt  4971  resmpt  5052  mptresid  5058  mptcnv  5130  mptpreima  5221  funmpt  5355  dfmpt3  5445  mptfng  5448  mptun  5454  dffn5im  5678  fvmptss2  5708  fvmptg  5709  fndmin  5741  f1ompt  5785  fmptco  5800  mpomptx  6094  f1ocnvd  6206  f1od2  6379  dftpos4  6407  mapsncnv  6840