Theorem isfld 20790

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  CRingccrg 20284  DivRingcdr 20779  Fieldcfield 20780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-field 20782

This theorem is referenced by:  flddrngd  20791  fldcrngd  20792  fldpropd  20820  fldidom  20821  fiidomfld  20824  rng1nfld  20828  fldcat  20832  fldsdrgfld  20847  primefld  20854  ofldlt1  20924  subofld  20926  ofldchr  21628  refld  21671  frlmphllem  21832  frlmphl  21833  recvs  25208  rrxcph  25454  rrx0  25459  ply1pid  26243  lgseisenlem3  27441  lgseisenlem4  27442  isarchiofld  33379  qfld  33484  fracfld  33495  fldgenfld  33507  cnfldfld  33528  reofld  33529  rearchi  33532  qsfld  33686  srafldlvec  33883  assafld  33934  ccfldextrr  33943  fldextsralvec  33952  extdgcl  33953  extdggt0  33954  fldextid  33956  extdgid  33957  extdgmul  33960  extdg1id  33963  ccfldsrarelvec  33968  2sqr3minply  34077  qqhrhm  34286  matunitlindflem1  38115  matunitlindflem2  38116  matunitlindf  38117  fldhmf1  42707  aks6d1c1p2  42726  aks6d1c2lem4  42744  aks6d1c5lem3  42754  aks6d1c5lem2  42755  aks6d1c6lem1  42787  ricfld  43148  fldcatALTV  48953