Definition df-im

Description: Define a function whose value is the imaginary part of a complex number. See imval for its value, imcli for its closure, and replim for its use in decomposing a complex number. (Contributed by NM, 9-May-1999)

	Ref	Expression
Assertion	df-im	$$⊢\Im =\left(x\in ℂ⟼\Re \left(\frac{x}{\mathrm{i}}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cim	$$class\Im$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		cre	$$class\Re$$
4	1	cv	$$setvarx$$
5		cdiv	$$class÷$$
6		ci	$$class\mathrm{i}$$
7	4 6 5	co	$$class\left(\frac{x}{\mathrm{i}}\right)$$
8	7 3	cfv	$$class\Re \left(\frac{x}{\mathrm{i}}\right)$$
9	1 2 8	cmpt	$$class\left(x\in ℂ⟼\Re \left(\frac{x}{\mathrm{i}}\right)\right)$$
10	0 9	wceq	$$wff\Im =\left(x\in ℂ⟼\Re \left(\frac{x}{\mathrm{i}}\right)\right)$$