Metamath Proof Explorer


Theorem bj-flddrng

Description: Fields are division rings. (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-flddrng Field DivRing

Proof

Step Hyp Ref Expression
1 df-field Field = DivRing CRing
2 inss1 DivRing CRing DivRing
3 1 2 eqsstri Field DivRing