Definition df-ef 7503

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 7498	. 2 class exp
2		vx	. . . . . 6 set x
3	2	cv 991	. . . . 5 class x
4		cc 5386	. . . . 5 class CC
5	3, 4	wcel 994	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 991	. . . . 5 class y
8		cn0 5451	. . . . . 6 class NN0
9		vk	. . . . . . . . 9 set k
10	9	cv 991	. . . . . . . 8 class k
11		cexp 6763	. . . . . . . 8 class ^
12	3, 10, 11	co 4021	. . . . . . 7 class (x^k)
13		cfa 7134	. . . . . . . 8 class !
14	10, 13	cfv 3263	. . . . . . 7 class (!` k)
15		cdiv 5448	. . . . . . 7 class /
16	12, 14, 15	co 4021	. . . . . 6 class ((x^k) / (!` k))
17	8, 16, 9	csu 7182	. . . . 5 class sum_k e. NN0 ((x^k) / (!` k))
18	7, 17	wceq 992	. . . 4 wff y = sum_k e. NN0 ((x^k) / (!` k))
19	5, 18	wa 221	. . 3 wff (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))
20	19, 2, 6	copab 2740	. 2 class {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}
21	1, 20	wceq 992	1 wff exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}

This definition is referenced by:  efval 7513  eff 7518  reeff1 7618  reeff1o 7634

Copyright terms: Public domain