Definition df-mpo 6023

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 4152 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 6020	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1396	. . . . . 6 class x
8	7, 3	wcel 2202	. . . . 5 wff x e. A
9	2	cv 1396	. . . . . 6 class y
10	9, 4	wcel 2202	. . . . 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 1396	. . . . 5 class z
14	13, 5	wceq 1397	. . . 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 6019	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1397	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  6080  mpoeq123dva  6082  mpoeq3dva  6085  nfmpo1  6088  nfmpo2  6089  nfmpo  6090  mpo0  6091  cbvmpox  6099  mpov  6111  mpomptx  6112  resmpo  6119  mpofun  6123  mpo2eqb  6131  rnmpo  6132  reldmmpo  6133  ovmpt4g  6144  elmpocl  6217  fmpox  6365  f1od2  6400  elmpom  6403  tposmpo  6447  erovlem  6796  xpcomco  7010  dfplpq2  7574  dfmpq2  7575  mpomulf  8169