Definition df-mpt 3820

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 3818	. 2 class ( x e. A |-> B )
5	1	cv 1242	. . . . 5 class x
6	5, 2	wcel 1393	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1242	. . . . 5 class y
9	8, 3	wceq 1243	. . . 4 wff y = B
10	6, 9	wa 97	. . 3 wff ( x e. A /\ y = B )
11	10, 1, 7	copab 3817	. 2 class { <. x , y >. | ( x e. A /\ y = B ) }
12	4, 11	wceq 1243	1 wff ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

This definition is referenced by:  mpteq12f  3837  nfmpt  3849  nfmpt1  3850  cbvmpt  3851  mptv  3853  fconstmpt  4387  rnmpt  4582  resmpt  4656  mptresid  4660  mptpreima  4814  funmpt  4938  dfmpt3  5021  mptfng  5024  mptun  5029  dffn5im  5219  fvmptss2  5247  fvmptg  5248  fndmin  5274  f1ompt  5320  fmptco  5330  mpt2mptx  5595  f1ocnvd  5702  dftpos4  5878