Theorem isfld 20660

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20154  DivRingcdr 20649  Fieldcfield 20650

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 3446  df-in 3918  df-field 20652

This theorem is referenced by:  flddrngd  20661  fldcrngd  20662  fldpropd  20690  fldidom  20691  fiidomfld  20694  rng1nfld  20699  fldcat  20703  fldsdrgfld  20718  primefld  20725  ofldlt1  20795  subofld  20797  ofldchr  21518  refld  21561  frlmphllem  21722  frlmphl  21723  recvs  25079  rrxcph  25325  rrx0  25330  ply1pid  26121  lgseisenlem3  27321  lgseisenlem4  27322  isarchiofld  33168  qfld  33263  fracfld  33274  fldgenfld  33286  cnfldfld  33307  reofld  33308  rearchi  33310  qsfld  33462  srafldlvec  33575  rgmoddimOLD  33599  assafld  33626  ccfldextrr  33635  fldextsralvec  33644  extdgcl  33645  extdggt0  33646  fldextid  33648  extdgid  33649  extdgmul  33652  extdg1id  33654  ccfldsrarelvec  33659  2sqr3minply  33763  qqhrhm  33972  matunitlindflem1  37603  matunitlindflem2  37604  matunitlindf  37605  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c2lem4  42108  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c6lem1  42151  ricfld  42511  fldcatALTV  48312