Definition df-mpo 5939

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 4106 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 5936	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1371	. . . . . 6 class x
8	7, 3	wcel 2175	. . . . 5 wff x e. A
9	2	cv 1371	. . . . . 6 class y
10	9, 4	wcel 2175	. . . . 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 1371	. . . . 5 class z
14	13, 5	wceq 1372	. . . 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 5935	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1372	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  5994  mpoeq123dva  5996  mpoeq3dva  5999  nfmpo1  6002  nfmpo2  6003  nfmpo  6004  mpo0  6005  cbvmpox  6013  mpov  6025  mpomptx  6026  resmpo  6033  mpofun  6037  mpo2eqb  6045  rnmpo  6046  reldmmpo  6047  ovmpt4g  6058  elmpocl  6131  fmpox  6276  f1od2  6311  tposmpo  6357  erovlem  6704  xpcomco  6903  dfplpq2  7449  dfmpq2  7450  mpomulf  8044