Theorem bj-flddrng

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

	Ref	Expression
Assertion	bj-flddrng	$$⊢F\in \mathrm{Field}\to F\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		bj-fldssdrng	$$⊢\mathrm{Field}\subseteq \mathrm{DivRing}$$
2	1	sseli	$$⊢F\in \mathrm{Field}\to F\in \mathrm{DivRing}$$