MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfld Structured version   Visualization version   GIF version

Theorem isfld 18579
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isfld (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Proof of Theorem isfld
StepHypRef Expression
1 df-field 18573 . 2 Field = (DivRing ∩ CRing)
21elin2 3763 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wcel 1977  CRingccrg 18371  DivRingcdr 18570  Fieldcfield 18571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-field 18573
This theorem is referenced by:  fldpropd  18598  rng1nfld  19099  fldidom  19126  fiidomfld  19129  refld  19784  recrng  19786  frlmphllem  19938  frlmphl  19939  rrxcph  22988  ply1pid  23743  lgseisenlem3  24902  lgseisenlem4  24903  ofldlt1  29144  ofldchr  29145  subofld  29147  isarchiofld  29148  reofld  29171  rearchi  29173  qqhrhm  29361  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  fldcat  41874  fldcatALTV  41893
  Copyright terms: Public domain W3C validator