Metamath Proof Explorer

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 i^i Com2 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfld 
 |-  Fld
1 cdrng 
 |-  DivRingOps
2 ccm2 
 |-  Com2
3 1 2 cin 
 |-  ( DivRingOps i^i Com2 )
4 0 3 wceq 
 |-  Fld = ( DivRingOps i^i Com2 )