Theorem isfld 20740

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20231  DivRingcdr 20729  Fieldcfield 20730

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-field 20732

This theorem is referenced by:  flddrngd  20741  fldcrngd  20742  fldpropd  20770  fldidom  20771  fldidomOLD  20772  fiidomfld  20775  rng1nfld  20780  fldcat  20784  fldsdrgfld  20799  primefld  20806  refld  21637  frlmphllem  21800  frlmphl  21801  recvs  25179  rrxcph  25426  rrx0  25431  ply1pid  26222  lgseisenlem3  27421  lgseisenlem4  27422  qfld  33300  fracfld  33310  fldgenfld  33322  ofldlt1  33343  ofldchr  33344  subofld  33346  isarchiofld  33347  cnfldfld  33371  reofld  33372  rearchi  33374  qsfld  33526  srafldlvec  33637  rgmoddimOLD  33661  assafld  33688  ccfldextrr  33699  fldextsralvec  33706  extdgcl  33707  extdggt0  33708  fldextid  33710  extdgid  33711  extdgmul  33714  extdg1id  33716  ccfldsrarelvec  33721  2sqr3minply  33791  qqhrhm  33990  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  fldhmf1  42091  aks6d1c1p2  42110  aks6d1c2lem4  42128  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c6lem1  42171  ricfld  42540  fldcatALTV  48247