Metamath Proof Explorer

Theorem bj-flddrng

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

Ref Expression
Assertion bj-flddrng 
|- Field C_ DivRing

Proof

Step Hyp Ref Expression
1 df-field 
 |-  Field = ( DivRing i^i CRing )
2 inss1 
 |-  ( DivRing i^i CRing ) C_ DivRing
3 1 2 eqsstri 
 |-  Field C_ DivRing