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

Theorem isfld 18950
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 18944 . 2 Field = (DivRing ∩ CRing)
21elin2 3936 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wcel 2131  CRingccrg 18740  DivRingcdr 18941  Fieldcfield 18942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-in 3714  df-field 18944
This theorem is referenced by:  fldpropd  18969  rng1nfld  19472  fldidom  19499  fiidomfld  19502  refld  20159  recrng  20161  frlmphllem  20313  frlmphl  20314  rrxcph  23372  ply1pid  24130  lgseisenlem3  25293  lgseisenlem4  25294  ofldlt1  30114  ofldchr  30115  subofld  30117  isarchiofld  30118  reofld  30141  rearchi  30143  qqhrhm  30334  matunitlindflem1  33710  matunitlindflem2  33711  matunitlindf  33712  fldcat  42584  fldcatALTV  42602
  Copyright terms: Public domain W3C validator