Definition df-mpt

Description: Define maps-to notation for defining a function via a rule. Read as "the function which maps x (in A ) to B ( x ) ". The class expression B is the value of the function at x and normally contains the variable x . An example is the square function for complex numbers, ( x e. CC |-> ( x ^ 2 ) ) . Similar to the definition of mapping in ChoquetDD p. 2. (Contributed by NM, 17-Feb-2008)

	Ref	Expression
Assertion	df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		cB	|- B
3	0 1 2	cmpt	|- ( x e. A |-> B )
4		vy	|- y
5	0	cv	|- x
6	5 1	wcel	|- x e. A
7	4	cv	|- y
8	7 2	wceq	|- y = B
9	6 8	wa	|- ( x e. A /\ y = B )
10	9 0 4	copab	|- { <. x , y >. | ( x e. A /\ y = B ) }
11	3 10	wceq	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }