Theorem isfld 20711

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  CRingccrg 20209  DivRingcdr 20700  Fieldcfield 20701

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 3432  df-in 3897  df-field 20703

This theorem is referenced by:  flddrngd  20712  fldcrngd  20713  fldpropd  20741  fldidom  20742  fiidomfld  20745  rng1nfld  20750  fldcat  20754  fldsdrgfld  20769  primefld  20776  ofldlt1  20846  subofld  20848  ofldchr  21569  refld  21612  frlmphllem  21773  frlmphl  21774  recvs  25126  rrxcph  25372  rrx0  25377  ply1pid  26161  lgseisenlem3  27357  lgseisenlem4  27358  isarchiofld  33278  qfld  33376  fracfld  33387  fldgenfld  33399  cnfldfld  33420  reofld  33421  rearchi  33424  qsfld  33576  srafldlvec  33748  rgmoddimOLD  33773  assafld  33800  ccfldextrr  33809  fldextsralvec  33818  extdgcl  33819  extdggt0  33820  fldextid  33822  extdgid  33823  extdgmul  33826  extdg1id  33829  ccfldsrarelvec  33834  2sqr3minply  33943  qqhrhm  34152  matunitlindflem1  37954  matunitlindflem2  37955  matunitlindf  37956  fldhmf1  42546  aks6d1c1p2  42565  aks6d1c2lem4  42583  aks6d1c5lem3  42593  aks6d1c5lem2  42594  aks6d1c6lem1  42626  ricfld  42992  fldcatALTV  48822