Definition df-tan

Description: Define the tangent function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . (Contributed by Mario Carneiro, 14-Mar-2014)

	Ref	Expression
Assertion	df-tan	$$⊢\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctan	$$class\tan$$
1		vx	$$setvarx$$
2		ccos	$$class\cos$$
3	2	ccnv	$$class{\cos }^{-1}$$
4		cc	$$classℂ$$
5		cc0	$$class0$$
6	5	csn	$$class\left\{0\right\}$$
7	4 6	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
8	3 7	cima	$$class{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
9		csin	$$class\sin$$
10	1	cv	$$setvarx$$
11	10 9	cfv	$$class\sin x$$
12		cdiv	$$class÷$$
13	10 2	cfv	$$class\cos x$$
14	11 13 12	co	$$class\left(\frac{\sin x}{\cos x}\right)$$
15	1 8 14	cmpt	$$class\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$
16	0 15	wceq	$$wff\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$