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

Theorem isfld 18033
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 18027 . 2  |- Field  =  (
DivRing  i^i  CRing )
21elin2 3633 1  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    e. wcel 1898   CRingccrg 17830   DivRingcdr 18024  Fieldcfield 18025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-field 18027
This theorem is referenced by:  fldpropd  18052  rng1nfld  18551  fldidom  18578  fiidomfld  18581  refld  19236  recrng  19238  frlmphllem  19387  frlmphl  19388  rrxcph  22400  ply1pid  23186  lgseisenlem3  24328  lgseisenlem4  24329  ofldlt1  28625  ofldchr  28626  subofld  28628  isarchiofld  28629  reofld  28652  rearchi  28654  qqhrhm  28842  fldcat  40357  fldcatALTV  40376
  Copyright terms: Public domain W3C validator