Definition df-abs

Description: Define the function for the absolute value (modulus) of a complex number. See abscli for its closure and absval or absval2i for its value. For example, ( abs-u 2 ) = 2 ( ex-abs ). (Contributed by NM, 27-Jul-1999)

	Ref	Expression
Assertion	df-abs	$$⊢\mathrm{abs}=\left(x\in ℂ⟼\sqrt{x\bar{x}}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabs	$$class\mathrm{abs}$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		csqrt	$$class\surd$$
4	1	cv	$$setvarx$$
5		cmul	$$class\times$$
6		ccj	$$class*$$
7	4 6	cfv	$$class\bar{x}$$
8	4 7 5	co	$$classx\bar{x}$$
9	8 3	cfv	$$class\sqrt{x\bar{x}}$$
10	1 2 9	cmpt	$$class\left(x\in ℂ⟼\sqrt{x\bar{x}}\right)$$
11	0 10	wceq	$$wff\mathrm{abs}=\left(x\in ℂ⟼\sqrt{x\bar{x}}\right)$$