Metamath Proof Explorer


Theorem bj-flddrng

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

Ref Expression
Assertion bj-flddrng ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 bj-fldssdrng Field ⊆ DivRing
2 1 sseli ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )