Theorem isfld 20649

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20143  DivRingcdr 20638  Fieldcfield 20639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-field 20641

This theorem is referenced by:  flddrngd  20650  fldcrngd  20651  fldpropd  20679  fldidom  20680  fiidomfld  20683  rng1nfld  20688  fldcat  20692  fldsdrgfld  20707  primefld  20714  refld  21528  frlmphllem  21689  frlmphl  21690  recvs  25046  rrxcph  25292  rrx0  25297  ply1pid  26088  lgseisenlem3  27288  lgseisenlem4  27289  qfld  33247  fracfld  33258  fldgenfld  33270  ofldlt1  33291  ofldchr  33292  subofld  33294  isarchiofld  33295  cnfldfld  33314  reofld  33315  rearchi  33317  qsfld  33469  srafldlvec  33582  rgmoddimOLD  33606  assafld  33633  ccfldextrr  33642  fldextsralvec  33651  extdgcl  33652  extdggt0  33653  fldextid  33655  extdgid  33656  extdgmul  33659  extdg1id  33661  ccfldsrarelvec  33666  2sqr3minply  33770  qqhrhm  33979  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  fldhmf1  42078  aks6d1c1p2  42097  aks6d1c2lem4  42115  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c6lem1  42158  ricfld  42518  fldcatALTV  48319