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	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	cmpt	$$class\left(x\in A⟼B\right)$$
4		vy	$$setvary$$
5	0	cv	$$setvarx$$
6	5 1	wcel	$$wffx\in A$$
7	4	cv	$$setvary$$
8	7 2	wceq	$$wffy=B$$
9	6 8	wa	$$wff\left(x\in A\wedge y=B\right)$$
10	9 0 4	copab	$$class\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
11	3 10	wceq	$$wff\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$