Definition df-field

Description: Afield is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015)

	Ref	Expression
Assertion	df-field	⊢ Field = ( DivRing ∩ CRing )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfield	⊢ Field
1		cdr	⊢ DivRing
2		ccrg	⊢ CRing
3	1 2	cin	⊢ ( DivRing ∩ CRing )
4	0 3	wceq	⊢ Field = ( DivRing ∩ CRing )