Definition df-mpt 4093

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

This definition is referenced by:  mpteq12f  4110  nfmpt  4122  nfmpt1  4123  cbvmptf  4124  cbvmpt  4125  mptv  4127  fconstmpt  4707  mptrel  4791  rnmpt  4911  resmpt  4991  mptresid  4997  mptcnv  5069  mptpreima  5160  funmpt  5293  dfmpt3  5377  mptfng  5380  mptun  5386  dffn5im  5603  fvmptss2  5633  fvmptg  5634  fndmin  5666  f1ompt  5710  fmptco  5725  mpomptx  6010  f1ocnvd  6122  f1od2  6290  dftpos4  6318  mapsncnv  6751