Definition df-ef 7298

Description: Define the exponential function.

Assertion

Ref	Expression
df-ef	|- exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}

Distinct variable group:   x,k,y

Detailed syntax breakdown of Definition df-ef

Step	Hyp	Ref	Expression
1		ce 7293	. 2 class exp
2		vx	. . . . . 6 set x
3	2	cv 955	. . . . 5 class x
4		cc 5232	. . . . 5 class CC
5	3, 4	wcel 958	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 955	. . . . 5 class y
8		cn0 5297	. . . . . 6 class NN0
9		vk	. . . . . . . . 9 set k
10	9	cv 955	. . . . . . . 8 class k
11		cexp 6568	. . . . . . . 8 class ^
12	3, 10, 11	co 3963	. . . . . . 7 class (x^k)
13		cfa 6931	. . . . . . . 8 class !
14	10, 13	cfv 3182	. . . . . . 7 class (!` k)
15		cdiv 5294	. . . . . . 7 class /
16	12, 14, 15	co 3963	. . . . . 6 class ((x^k) / (!` k))
17	8, 16, 9	csu 6979	. . . . 5 class sum_k e. NN0 ((x^k) / (!` k))
18	7, 17	wceq 956	. . . 4 wff y = sum_k e. NN0 ((x^k) / (!` k))
19	5, 18	wa 223	. . 3 wff (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))
20	19, 2, 6	copab 2666	. 2 class {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}
21	1, 20	wceq 956	1 wff exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}

This definition is referenced by:  efvalt 7308  eff 7313  reeff1 7410  reeff1o 7426

Copyright terms: Public domain