Definition df-mpo 6018

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 4150 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 6015	. 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 6014	. 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  6075  mpoeq123dva  6077  mpoeq3dva  6080  nfmpo1  6083  nfmpo2  6084  nfmpo  6085  mpo0  6086  cbvmpox  6094  mpov  6106  mpomptx  6107  resmpo  6114  mpofun  6118  mpo2eqb  6126  rnmpo  6127  reldmmpo  6128  ovmpt4g  6139  elmpocl  6212  fmpox  6360  f1od2  6395  elmpom  6398  tposmpo  6442  erovlem  6791  xpcomco  7005  dfplpq2  7564  dfmpq2  7565  mpomulf  8159