Theorem isfld 20685

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  CRingccrg 20181  DivRingcdr 20674  Fieldcfield 20675

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-field 20677

This theorem is referenced by:  flddrngd  20686  fldcrngd  20687  fldpropd  20715  fldidom  20716  fiidomfld  20719  rng1nfld  20724  fldcat  20728  fldsdrgfld  20743  primefld  20750  ofldlt1  20820  subofld  20822  ofldchr  21543  refld  21586  frlmphllem  21747  frlmphl  21748  recvs  25114  rrxcph  25360  rrx0  25365  ply1pid  26156  lgseisenlem3  27356  lgseisenlem4  27357  isarchiofld  33293  qfld  33391  fracfld  33402  fldgenfld  33414  cnfldfld  33435  reofld  33436  rearchi  33439  qsfld  33591  srafldlvec  33763  rgmoddimOLD  33788  assafld  33815  ccfldextrr  33824  fldextsralvec  33833  extdgcl  33834  extdggt0  33835  fldextid  33837  extdgid  33838  extdgmul  33841  extdg1id  33844  ccfldsrarelvec  33849  2sqr3minply  33958  qqhrhm  34167  matunitlindflem1  37867  matunitlindflem2  37868  matunitlindf  37869  fldhmf1  42460  aks6d1c1p2  42479  aks6d1c2lem4  42497  aks6d1c5lem3  42507  aks6d1c5lem2  42508  aks6d1c6lem1  42540  ricfld  42900  fldcatALTV  48691