Theorem flddivrng

Description: A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	flddivrng	$$⊢K\in \mathrm{Fld}\to K\in \mathrm{DivRingOps}$$

Proof

Step	Hyp	Ref	Expression
1		df-fld	$$⊢\mathrm{Fld}=\mathrm{DivRingOps}\cap \mathrm{Com2}$$
2		inss1	$$⊢\mathrm{DivRingOps}\cap \mathrm{Com2}\subseteq \mathrm{DivRingOps}$$
3	1 2	eqsstri	$$⊢\mathrm{Fld}\subseteq \mathrm{DivRingOps}$$
4	3	sseli	$$⊢K\in \mathrm{Fld}\to K\in \mathrm{DivRingOps}$$