Definition df-mpo 6005

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 4146 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 6002	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1394	. . . . . 6 class x
8	7, 3	wcel 2200	. . . . 5 wff x e. A
9	2	cv 1394	. . . . . 6 class y
10	9, 4	wcel 2200	. . . . 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 1394	. . . . 5 class z
14	13, 5	wceq 1395	. . . 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 6001	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1395	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  6062  mpoeq123dva  6064  mpoeq3dva  6067  nfmpo1  6070  nfmpo2  6071  nfmpo  6072  mpo0  6073  cbvmpox  6081  mpov  6093  mpomptx  6094  resmpo  6101  mpofun  6105  mpo2eqb  6113  rnmpo  6114  reldmmpo  6115  ovmpt4g  6126  elmpocl  6199  fmpox  6344  f1od2  6379  tposmpo  6425  erovlem  6772  xpcomco  6981  dfplpq2  7537  dfmpq2  7538  mpomulf  8132