Theorem isfld 19504

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 19498	. 2 ⊢ Field = (DivRing ∩ CRing)
2	1	elin2 4124	1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  CRingccrg 19291  DivRingcdr 19495  Fieldcfield 19496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-field 19498

This theorem is referenced by:  fldpropd  19523  primefld  19577  rng1nfld  20044  fldidom  20071  fiidomfld  20074  refld  20308  recrng  20310  frlmphllem  20469  frlmphl  20470  rrxcph  23996  rrx0  24001  ply1pid  24780  lgseisenlem3  25961  lgseisenlem4  25962  ofldlt1  30937  ofldchr  30938  subofld  30940  isarchiofld  30941  reofld  30964  rearchi  30966  srafldlvec  31079  rgmoddim  31096  ccfldextrr  31126  fldextsralvec  31133  extdgcl  31134  extdggt0  31135  fldextid  31137  extdgmul  31139  extdg1id  31141  ccfldsrarelvec  31144  qqhrhm  31340  matunitlindflem1  35053  matunitlindflem2  35054  matunitlindf  35055  fldcat  44706  fldcatALTV  44724