Definition df-mpo 5880

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 B ( x , y )". An extension of df-mpt 4067 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

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

Distinct variable groups:   x, z   y, z   z, A   z, B   z, C

Allowed substitution hints:   A( x, y)   B( x, y)   C( x, y)

Detailed syntax breakdown of Definition df-mpo

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

This definition is referenced by:  mpoeq123  5934  mpoeq123dva  5936  mpoeq3dva  5939  nfmpo1  5942  nfmpo2  5943  nfmpo  5944  mpo0  5945  cbvmpox  5953  mpov  5965  mpomptx  5966  resmpo  5973  mpofun  5977  mpo2eqb  5984  rnmpo  5985  reldmmpo  5986  ovmpt4g  5997  elmpocl  6069  fmpox  6201  f1od2  6236  tposmpo  6282  erovlem  6627  xpcomco  6826  dfplpq2  7353  dfmpq2  7354