Definition df-mpo 5948

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 5945	. 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 5944	. 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  6003  mpoeq123dva  6005  mpoeq3dva  6008  nfmpo1  6011  nfmpo2  6012  nfmpo  6013  mpo0  6014  cbvmpox  6022  mpov  6034  mpomptx  6035  resmpo  6042  mpofun  6046  mpo2eqb  6054  rnmpo  6055  reldmmpo  6056  ovmpt4g  6067  elmpocl  6140  fmpox  6285  f1od2  6320  tposmpo  6366  erovlem  6713  xpcomco  6920  dfplpq2  7466  dfmpq2  7467  mpomulf  8061