Definition df-mpo 5879

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 4066 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 5876	. 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 5875	. 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  5933  mpoeq123dva  5935  mpoeq3dva  5938  nfmpo1  5941  nfmpo2  5942  nfmpo  5943  mpo0  5944  cbvmpox  5952  mpov  5964  mpomptx  5965  resmpo  5972  mpofun  5976  mpo2eqb  5983  rnmpo  5984  reldmmpo  5985  ovmpt4g  5996  elmpocl  6068  fmpox  6200  f1od2  6235  tposmpo  6281  erovlem  6626  xpcomco  6825  dfplpq2  7352  dfmpq2  7353