Definition df-mpo

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B ) to C ( x , y ) ". An extension of df-mpt for two arguments. (Contributed by NM, 17-Feb-2008)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		vy	|- y
3		cB	|- B
4		cC	|- C
5	0 2 1 3 4	cmpo	|- ( x e. A , y e. B |-> C )
6		vz	|- z
7	0	cv	|- x
8	7 1	wcel	|- x e. A
9	2	cv	|- y
10	9 3	wcel	|- y e. B
11	8 10	wa	|- ( x e. A /\ y e. B )
12	6	cv	|- z
13	12 4	wceq	|- z = C
14	11 13	wa	|- ( ( x e. A /\ y e. B ) /\ z = C )
15	14 0 2 6	coprab	|- { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
16	5 15	wceq	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }