Theorem isfld 19981

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2109  CRingccrg 19765  DivRingcdr 19972  Fieldcfield 19973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-field 19975

This theorem is referenced by:  fldpropd  20000  primefld  20054  rng1nfld  20530  fldidom  20557  fldidomOLD  20558  fiidomfld  20561  refld  20805  recrng  20807  frlmphllem  20968  frlmphl  20969  recvs  24290  rrxcph  24537  rrx0  24542  ply1pid  25325  lgseisenlem3  26506  lgseisenlem4  26507  ofldlt1  31491  ofldchr  31492  subofld  31494  isarchiofld  31495  reofld  31523  rearchi  31525  srafldlvec  31655  rgmoddim  31672  ccfldextrr  31702  fldextsralvec  31709  extdgcl  31710  extdggt0  31711  fldextid  31713  extdgmul  31715  extdg1id  31717  ccfldsrarelvec  31720  qqhrhm  31918  matunitlindflem1  35752  matunitlindflem2  35753  matunitlindf  35754  fldcrngd  40235  prjcrv0  40450  fldcat  45592  fldcatALTV  45610