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	⊢ Fld = ( DivRingOps ∩ Com2 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfld	⊢ Fld
1		cdrng	⊢ DivRingOps
2		ccm2	⊢ Com2
3	1 2	cin	⊢ ( DivRingOps ∩ Com2 )
4	0 3	wceq	⊢ Fld = ( DivRingOps ∩ Com2 )