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, 4-Apr-2009) (Revised by NM, 18-Oct-2012)

	Ref	Expression
Assertion	df-drng	⊢ DivRing = { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdr	⊢ DivRing
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		cui	⊢ Unit
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( Unit ‘ 𝑟 )
6		cbs	⊢ Base
7	4 6	cfv	⊢ ( Base ‘ 𝑟 )
8		c0g	⊢ 0g
9	4 8	cfv	⊢ ( 0g ‘ 𝑟 )
10	9	csn	⊢ { ( 0g ‘ 𝑟 ) }
11	7 10	cdif	⊢ ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } )
12	5 11	wceq	⊢ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } )
13	12 1 2	crab	⊢ { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) }
14	0 13	wceq	⊢ DivRing = { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) }