Definition df-mpo 5779

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 3991 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 5776	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1330	. . . . . 6 class x
8	7, 3	wcel 1480	. . . . 5 wff x e. A
9	2	cv 1330	. . . . . 6 class y
10	9, 4	wcel 1480	. . . . 5 wff y e. B
11	8, 10	wa 103	. . . 4 wff ( x e. A /\ y e. B )
12		vz	. . . . . 6 setvar z
13	12	cv 1330	. . . . 5 class z
14	13, 5	wceq 1331	. . . 4 wff z = C
15	11, 14	wa 103	. . 3 wff ( ( x e. A /\ y e. B ) /\ z = C )
16	15, 1, 2, 12	coprab 5775	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1331	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  5830  mpoeq123dva  5832  mpoeq3dva  5835  nfmpo1  5838  nfmpo2  5839  nfmpo  5840  mpo0  5841  cbvmpox  5849  mpov  5861  mpomptx  5862  resmpo  5869  mpofun  5873  mpo2eqb  5880  rnmpo  5881  reldmmpo  5882  ovmpt4g  5893  elmpocl  5968  fmpox  6098  f1od2  6132  tposmpo  6178  erovlem  6521  xpcomco  6720  dfplpq2  7162  dfmpq2  7163