Definition df-field

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

	Ref	Expression
Assertion	df-field	$$⊢\mathrm{Field}=\mathrm{DivRing}\cap \mathrm{CRing}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfield	$$class\mathrm{Field}$$
1		cdr	$$class\mathrm{DivRing}$$
2		ccrg	$$class\mathrm{CRing}$$
3	1 2	cin	$$class\left(\mathrm{DivRing}\cap \mathrm{CRing}\right)$$
4	0 3	wceq	$$wff\mathrm{Field}=\mathrm{DivRing}\cap \mathrm{CRing}$$