Theorem isfld 20625

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20119  DivRingcdr 20614  Fieldcfield 20615

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 3438  df-in 3910  df-field 20617

This theorem is referenced by:  flddrngd  20626  fldcrngd  20627  fldpropd  20655  fldidom  20656  fiidomfld  20659  rng1nfld  20664  fldcat  20668  fldsdrgfld  20683  primefld  20690  ofldlt1  20760  subofld  20762  ofldchr  21483  refld  21526  frlmphllem  21687  frlmphl  21688  recvs  25044  rrxcph  25290  rrx0  25295  ply1pid  26086  lgseisenlem3  27286  lgseisenlem4  27287  isarchiofld  33141  qfld  33236  fracfld  33247  fldgenfld  33259  cnfldfld  33280  reofld  33281  rearchi  33283  qsfld  33435  srafldlvec  33552  rgmoddimOLD  33577  assafld  33604  ccfldextrr  33613  fldextsralvec  33622  extdgcl  33623  extdggt0  33624  fldextid  33626  extdgid  33627  extdgmul  33630  extdg1id  33633  ccfldsrarelvec  33638  2sqr3minply  33747  qqhrhm  33956  matunitlindflem1  37600  matunitlindflem2  37601  matunitlindf  37602  fldhmf1  42067  aks6d1c1p2  42086  aks6d1c2lem4  42104  aks6d1c5lem3  42114  aks6d1c5lem2  42115  aks6d1c6lem1  42147  ricfld  42507  fldcatALTV  48319