Theorem isfld 19119

Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)

Assertion

Ref	Expression
isfld	⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Proof of Theorem isfld

Step	Hyp	Ref	Expression
1		df-field 19113	. 2 ⊢ Field = (DivRing ∩ CRing)
2	1	elin2 4030	1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Syntax hints:   ↔ wb 198   ∧ wa 386   ∈ wcel 2164  CRingccrg 18909  DivRingcdr 19110  Fieldcfield 19111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-field 19113

This theorem is referenced by:  fldpropd  19138  rng1nfld  19646  fldidom  19673  fiidomfld  19676  refld  20333  recrng  20335  frlmphllem  20493  frlmphl  20494  rrxcph  23567  rrx0  23572  ply1pid  24345  lgseisenlem3  25522  lgseisenlem4  25523  ofldlt1  30354  ofldchr  30355  subofld  30357  isarchiofld  30358  reofld  30381  rearchi  30383  qqhrhm  30574  matunitlindflem1  33944  matunitlindflem2  33945  matunitlindf  33946  fldcat  42943  fldcatALTV  42961