Definition df-mpt2 4080

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 4079 for two arguments.

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,y   y,A   y,B

Detailed syntax breakdown of Definition df-mpt2

Step	Hyp	Ref	Expression
1		vx	. . 3 set x
2		vy	. . 3 set y
3		cA	. . 3 class A
4		cB	. . 3 class B
5		cC	. . 3 class C
6	1, 2, 3, 4, 5	cmpt2 4078	. 2 class (x e. A, y e. B |-> C)
7	1	cv 957	. . . . . 6 class x
8	7, 3	wcel 960	. . . . 5 wff x e. A
9	2	cv 957	. . . . . 6 class y
10	9, 4	wcel 960	. . . . 5 wff y e. B
11	8, 10	wa 223	. . . 4 wff (x e. A /\ y e. B)
12		vz	. . . . . 6 set z
13	12	cv 957	. . . . 5 class z
14	13, 5	wceq 958	. . . 4 wff z = C
15	11, 14	wa 223	. . 3 wff ((x e. A /\ y e. B) /\ z = C)
16	15, 1, 2, 12	copab2 3970	. 2 class {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}
17	6, 16	wceq 958	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:  mpt2g 4082

Copyright terms: Public domain