Metamath Proof Explorer

Definition df-field

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

Ref Expression
Assertion df-field 
|- Field = ( DivRing i^i CRing )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfield 
 |-  Field
1 cdr 
 |-  DivRing
2 ccrg 
 |-  CRing
3 1 2 cin 
 |-  ( DivRing i^i CRing )
4 0 3 wceq 
 |-  Field = ( DivRing i^i CRing )