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	|- DivRing = { r e. Ring | ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdr	|- DivRing
1		vr	|- r
2		crg	|- Ring
3		cui	|- Unit
4	1	cv	|- r
5	4 3	cfv	|- ( Unit ` r )
6		cbs	|- Base
7	4 6	cfv	|- ( Base ` r )
8		c0g	|- 0g
9	4 8	cfv	|- ( 0g ` r )
10	9	csn	|- { ( 0g ` r ) }
11	7 10	cdif	|- ( ( Base ` r ) \ { ( 0g ` r ) } )
12	5 11	wceq	|- ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } )
13	12 1 2	crab	|- { r e. Ring | ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
14	0 13	wceq	|- DivRing = { r e. Ring | ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }