Definition df-mpt 4115

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

This definition is referenced by:  mpteq12f  4132  nfmpt  4144  nfmpt1  4145  cbvmptf  4146  cbvmpt  4147  mptv  4149  fconstmpt  4730  mptrel  4814  rnmpt  4935  resmpt  5016  mptresid  5022  mptcnv  5094  mptpreima  5185  funmpt  5318  dfmpt3  5408  mptfng  5411  mptun  5417  dffn5im  5637  fvmptss2  5667  fvmptg  5668  fndmin  5700  f1ompt  5744  fmptco  5759  mpomptx  6049  f1ocnvd  6161  f1od2  6334  dftpos4  6362  mapsncnv  6795