Definition df-cosh

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

	Ref	Expression
Assertion	df-cosh	$$⊢\cosh =\left(x\in ℂ⟼\cos \mathrm{i}x\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccosh	$$class\cosh$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		ccos	$$class\cos$$
4		ci	$$class\mathrm{i}$$
5		cmul	$$class\times$$
6	1	cv	$$setvarx$$
7	4 6 5	co	$$class\mathrm{i}x$$
8	7 3	cfv	$$class\cos \mathrm{i}x$$
9	1 2 8	cmpt	$$class\left(x\in ℂ⟼\cos \mathrm{i}x\right)$$
10	0 9	wceq	$$wff\cosh =\left(x\in ℂ⟼\cos \mathrm{i}x\right)$$