Definition df-mpt 4106

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

This definition is referenced by:  mpteq12f  4123  nfmpt  4135  nfmpt1  4136  cbvmptf  4137  cbvmpt  4138  mptv  4140  fconstmpt  4721  mptrel  4805  rnmpt  4925  resmpt  5006  mptresid  5012  mptcnv  5084  mptpreima  5175  funmpt  5308  dfmpt3  5397  mptfng  5400  mptun  5406  dffn5im  5623  fvmptss2  5653  fvmptg  5654  fndmin  5686  f1ompt  5730  fmptco  5745  mpomptx  6035  f1ocnvd  6147  f1od2  6320  dftpos4  6348  mapsncnv  6781