This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 Fld \to K \in DivRingOps$

Proof

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