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 = ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( i · 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccosh	⊢ cosh
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		ccos	⊢ cos
4		ci	⊢ i
5		cmul	⊢ ·
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( i · 𝑥 )
8	7 3	cfv	⊢ ( cos ‘ ( i · 𝑥 ) )
9	1 2 8	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( i · 𝑥 ) ) )
10	0 9	wceq	⊢ cosh = ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( i · 𝑥 ) ) )