Definition df-cosh 42475

Description: Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4729, which requires the form ( x e. A |-> B ). (Contributed by David A. Wheeler, 10-May-2015.)

Assertion

Ref	Expression
df-cosh	|- cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )

Detailed syntax breakdown of Definition df-cosh

Step	Hyp	Ref	Expression
1		ccosh 42472	. 2 class cosh
2		vx	. . 3 setvar x
3		cc 9934	. . 3 class CC
4		ci 9938	. . . . 5 class _i
5	2	cv 1482	. . . . 5 class x
6		cmul 9941	. . . . 5 class x.
7	4, 5, 6	co 6650	. . . 4 class ( _i x. x )
8		ccos 14795	. . . 4 class cos
9	7, 8	cfv 5888	. . 3 class ( cos ` ( _i x. x ) )
10	2, 3, 9	cmpt 4729	. 2 class ( x e. CC |-> ( cos ` ( _i x. x ) ) )
11	1, 10	wceq 1483	1 wff cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )

This definition is referenced by:  coshval-named  42478