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

Step	Hyp	Ref	Expression
1		df-field 18027	. 2 |- Field = ( DivRing i^i CRing )
2	1	elin2 3633	1 |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

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