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

Theorem isfld 19119
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 19113 . 2 Field = (DivRing ∩ CRing)
21elin2 4030 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  wcel 2164  CRingccrg 18909  DivRingcdr 19110  Fieldcfield 19111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-field 19113
This theorem is referenced by:  fldpropd  19138  rng1nfld  19646  fldidom  19673  fiidomfld  19676  refld  20333  recrng  20335  frlmphllem  20493  frlmphl  20494  rrxcph  23567  rrx0  23572  ply1pid  24345  lgseisenlem3  25522  lgseisenlem4  25523  ofldlt1  30354  ofldchr  30355  subofld  30357  isarchiofld  30358  reofld  30381  rearchi  30383  qqhrhm  30574  matunitlindflem1  33944  matunitlindflem2  33945  matunitlindf  33946  fldcat  42943  fldcatALTV  42961
  Copyright terms: Public domain W3C validator