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