Definition df-drng

Description: Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012)

	Ref	Expression
Assertion	df-drng	$$⊢\mathrm{DivRing}=\left\{r\in \mathrm{Ring}|\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdr	$$class\mathrm{DivRing}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		cui	$$class\mathrm{Unit}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class\mathrm{Unit}\left(r\right)$$
6		cbs	$$class\mathrm{Base}$$
7	4 6	cfv	$$class{\mathrm{Base}}_r$$
8		c0g	$$class{0}_{𝑔}$$
9	4 8	cfv	$$class{0}_r$$
10	9	csn	$$class\left\{0_r\right\}$$
11	7 10	cdif	$$class\left({\mathrm{Base}}_r\setminus \left\{0_r\right\}\right)$$
12	5 11	wceq	$$wff\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}$$
13	12 1 2	crab	$$class\left\{r\in \mathrm{Ring}|\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}\right\}$$
14	0 13	wceq	$$wff\mathrm{DivRing}=\left\{r\in \mathrm{Ring}|\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}\right\}$$