Definition df-mpt2 5544

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 3847 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

Ref	Expression
df-mpt2	|- ( 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-mpt2

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	cmpt2 5541	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1258	. . . . . 6 class x
8	7, 3	wcel 1409	. . . . 5 wff x e. A
9	2	cv 1258	. . . . . 6 class y
10	9, 4	wcel 1409	. . . . 5 wff y e. B
11	8, 10	wa 101	. . . 4 wff ( x e. A /\ y e. B )
12		vz	. . . . . 6 setvar z
13	12	cv 1258	. . . . 5 class z
14	13, 5	wceq 1259	. . . 4 wff z = C
15	11, 14	wa 101	. . 3 wff ( ( x e. A /\ y e. B ) /\ z = C )
16	15, 1, 2, 12	coprab 5540	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1259	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:  mpt2eq123  5591  mpt2eq123dva  5593  mpt2eq3dva  5596  nfmpt21  5598  nfmpt22  5599  nfmpt2  5600  mpt20  5601  cbvmpt2x  5609  mpt2v  5621  mpt2mptx  5622  resmpt2  5626  mpt2fun  5630  mpt22eqb  5637  rnmpt2  5638  reldmmpt2  5639  ovmpt4g  5650  elmpt2cl  5725  fmpt2x  5853  f1od2  5883  tposmpt2  5926  erovlem  6228  xpcomco  6330  dfplpq2  6509  dfmpq2  6510