Metamath Proof Explorer

Theorem bj-flddrng

Description: Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024)

Ref Expression
Assertion bj-flddrng 
|- ( F e. Field -> F e. DivRing )

Proof

Step Hyp Ref Expression
1 bj-fldssdrng 
 |-  Field C_ DivRing
2 1 sseli 
 |-  ( F e. Field -> F e. DivRing )