Theorem isfld 20715

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∈ wcel 2121  CRingccrg 20209  DivRingcdr 20704  Fieldcfield 20705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3891  df-field 20707

This theorem is referenced by:  flddrngd  20716  fldcrngd  20717  fldpropd  20745  fldidom  20746  fiidomfld  20749  rng1nfld  20754  fldcat  20758  fldsdrgfld  20773  primefld  20780  ofldlt1  20850  subofld  20852  ofldchr  21554  refld  21597  frlmphllem  21758  frlmphl  21759  recvs  25134  rrxcph  25380  rrx0  25385  ply1pid  26169  lgseisenlem3  27361  lgseisenlem4  27362  isarchiofld  33282  qfld  33383  fracfld  33394  fldgenfld  33406  cnfldfld  33427  reofld  33428  rearchi  33431  qsfld  33583  srafldlvec  33780  assafld  33831  ccfldextrr  33840  fldextsralvec  33849  extdgcl  33850  extdggt0  33851  fldextid  33853  extdgid  33854  extdgmul  33857  extdg1id  33860  ccfldsrarelvec  33865  2sqr3minply  33974  qqhrhm  34183  matunitlindflem1  37996  matunitlindflem2  37997  matunitlindf  37998  fldhmf1  42588  aks6d1c1p2  42607  aks6d1c2lem4  42625  aks6d1c5lem3  42635  aks6d1c5lem2  42636  aks6d1c6lem1  42668  ricfld  43029  fldcatALTV  48834