Definition df-fld

Description: Definition of a field. A field is a commutative division ring. (Contributed by FL, 6-Sep-2009) (Revised by Jeff Madsen, 10-Jun-2010) (New usage is discouraged.)

	Ref	Expression
Assertion	df-fld	$$⊢\mathrm{Fld}=\mathrm{DivRingOps}\cap \mathrm{Com2}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfld	$$class\mathrm{Fld}$$
1		cdrng	$$class\mathrm{DivRingOps}$$
2		ccm2	$$class\mathrm{Com2}$$
3	1 2	cin	$$class\left(\mathrm{DivRingOps}\cap \mathrm{Com2}\right)$$
4	0 3	wceq	$$wff\mathrm{Fld}=\mathrm{DivRingOps}\cap \mathrm{Com2}$$