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

Theorem isfld 17919
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 17913 . 2  |- Field  =  (
DivRing  i^i  CRing )
21elin2 3659 1  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    e. wcel 1870   CRingccrg 17716   DivRingcdr 17910  Fieldcfield 17911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-field 17913
This theorem is referenced by:  fldpropd  17938  rng1nfld  18437  fldidom  18464  fiidomfld  18467  refld  19118  recrng  19120  frlmphllem  19269  frlmphl  19270  rrxcph  22244  ply1pid  23005  lgseisenlem3  24142  lgseisenlem4  24143  ofldlt1  28415  ofldchr  28416  subofld  28418  isarchiofld  28419  reofld  28442  rearchi  28444  qqhrhm  28632  fldcat  38841  fldcatALTV  38860
  Copyright terms: Public domain W3C validator