Definition df-mpo 5967

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 4118 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 5964	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1372	. . . . . 6 class x
8	7, 3	wcel 2177	. . . . 5 wff x e. A
9	2	cv 1372	. . . . . 6 class y
10	9, 4	wcel 2177	. . . . 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 1372	. . . . 5 class z
14	13, 5	wceq 1373	. . . 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 5963	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1373	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  6022  mpoeq123dva  6024  mpoeq3dva  6027  nfmpo1  6030  nfmpo2  6031  nfmpo  6032  mpo0  6033  cbvmpox  6041  mpov  6053  mpomptx  6054  resmpo  6061  mpofun  6065  mpo2eqb  6073  rnmpo  6074  reldmmpo  6075  ovmpt4g  6086  elmpocl  6159  fmpox  6304  f1od2  6339  tposmpo  6385  erovlem  6732  xpcomco  6941  dfplpq2  7497  dfmpq2  7498  mpomulf  8092