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 ( 𝐾 ∈ Fld → 𝐾 ∈ DivRingOps )

Proof

Step Hyp Ref Expression
1 df-fld Fld = ( DivRingOps ∩ Com2 )
2 inss1 ( DivRingOps ∩ Com2 ) ⊆ DivRingOps
3 1 2 eqsstri Fld ⊆ DivRingOps
4 3 sseli ( 𝐾 ∈ Fld → 𝐾 ∈ DivRingOps )