Description: Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-flddrng | ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-fldssdrng | ⊢ Field ⊆ DivRing | |
2 | 1 | sseli | ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing ) |