Definition df-mpt 4092

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 4090	. 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 4089	. 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  4109  nfmpt  4121  nfmpt1  4122  cbvmptf  4123  cbvmpt  4124  mptv  4126  fconstmpt  4706  mptrel  4790  rnmpt  4910  resmpt  4990  mptresid  4996  mptcnv  5068  mptpreima  5159  funmpt  5292  dfmpt3  5376  mptfng  5379  mptun  5385  dffn5im  5602  fvmptss2  5632  fvmptg  5633  fndmin  5665  f1ompt  5709  fmptco  5724  mpomptx  6009  f1ocnvd  6120  f1od2  6288  dftpos4  6316  mapsncnv  6749