Theorem isfld 20673

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  CRingccrg 20169  DivRingcdr 20662  Fieldcfield 20663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-field 20665

This theorem is referenced by:  flddrngd  20674  fldcrngd  20675  fldpropd  20703  fldidom  20704  fiidomfld  20707  rng1nfld  20712  fldcat  20716  fldsdrgfld  20731  primefld  20738  ofldlt1  20808  subofld  20810  ofldchr  21531  refld  21574  frlmphllem  21735  frlmphl  21736  recvs  25102  rrxcph  25348  rrx0  25353  ply1pid  26144  lgseisenlem3  27344  lgseisenlem4  27345  isarchiofld  33281  qfld  33379  fracfld  33390  fldgenfld  33402  cnfldfld  33423  reofld  33424  rearchi  33427  qsfld  33579  srafldlvec  33742  rgmoddimOLD  33767  assafld  33794  ccfldextrr  33803  fldextsralvec  33812  extdgcl  33813  extdggt0  33814  fldextid  33816  extdgid  33817  extdgmul  33820  extdg1id  33823  ccfldsrarelvec  33828  2sqr3minply  33937  qqhrhm  34146  matunitlindflem1  37817  matunitlindflem2  37818  matunitlindf  37819  fldhmf1  42354  aks6d1c1p2  42373  aks6d1c2lem4  42391  aks6d1c5lem3  42401  aks6d1c5lem2  42402  aks6d1c6lem1  42434  ricfld  42795  fldcatALTV  48587