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

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

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