Definition df-mpo 5847

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 4045 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 5844	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1342	. . . . . 6 class x
8	7, 3	wcel 2136	. . . . 5 wff x e. A
9	2	cv 1342	. . . . . 6 class y
10	9, 4	wcel 2136	. . . . 5 wff y e. B
11	8, 10	wa 103	. . . 4 wff ( x e. A /\ y e. B )
12		vz	. . . . . 6 setvar z
13	12	cv 1342	. . . . 5 class z
14	13, 5	wceq 1343	. . . 4 wff z = C
15	11, 14	wa 103	. . 3 wff ( ( x e. A /\ y e. B ) /\ z = C )
16	15, 1, 2, 12	coprab 5843	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1343	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  5901  mpoeq123dva  5903  mpoeq3dva  5906  nfmpo1  5909  nfmpo2  5910  nfmpo  5911  mpo0  5912  cbvmpox  5920  mpov  5932  mpomptx  5933  resmpo  5940  mpofun  5944  mpo2eqb  5951  rnmpo  5952  reldmmpo  5953  ovmpt4g  5964  elmpocl  6036  fmpox  6168  f1od2  6203  tposmpo  6249  erovlem  6593  xpcomco  6792  dfplpq2  7295  dfmpq2  7296