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

Theorem isfld 17927
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isfld  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )

Proof of Theorem isfld
StepHypRef Expression
1 df-field 17921 . 2  |- Field  =  (
DivRing  i^i  CRing )
21elin2 3596 1  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    e. wcel 1872   CRingccrg 17724   DivRingcdr 17918  Fieldcfield 17919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386  df-field 17921
This theorem is referenced by:  fldpropd  17946  rng1nfld  18445  fldidom  18472  fiidomfld  18475  refld  19129  recrng  19131  frlmphllem  19280  frlmphl  19281  rrxcph  22293  ply1pid  23079  lgseisenlem3  24221  lgseisenlem4  24222  ofldlt1  28528  ofldchr  28529  subofld  28531  isarchiofld  28532  reofld  28555  rearchi  28557  qqhrhm  28745  fldcat  39685  fldcatALTV  39704
  Copyright terms: Public domain W3C validator