Definition df-mpt2 5568

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 3861 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 5565	. 2 class ( x e. A , y e. B |-> C )
7	1	cv 1284	. . . . . 6 class x
8	7, 3	wcel 1434	. . . . 5 wff x e. A
9	2	cv 1284	. . . . . 6 class y
10	9, 4	wcel 1434	. . . . 5 wff y e. B
11	8, 10	wa 102	. . . 4 wff ( x e. A /\ y e. B )
12		vz	. . . . . 6 setvar z
13	12	cv 1284	. . . . 5 class z
14	13, 5	wceq 1285	. . . 4 wff z = C
15	11, 14	wa 102	. . 3 wff ( ( x e. A /\ y e. B ) /\ z = C )
16	15, 1, 2, 12	coprab 5564	. 2 class { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
17	6, 16	wceq 1285	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  5615  mpt2eq123dva  5617  mpt2eq3dva  5620  nfmpt21  5622  nfmpt22  5623  nfmpt2  5624  mpt20  5625  cbvmpt2x  5633  mpt2v  5645  mpt2mptx  5646  resmpt2  5650  mpt2fun  5654  mpt22eqb  5661  rnmpt2  5662  reldmmpt2  5663  ovmpt4g  5674  elmpt2cl  5749  fmpt2x  5877  f1od2  5907  tposmpt2  5950  erovlem  6285  xpcomco  6391  dfplpq2  6658  dfmpq2  6659