Theorem isfld 20236

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  CRingccrg 19979  DivRingcdr 20225  Fieldcfield 20226

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-field 20228

This theorem is referenced by:  fldcrngd  20237  fldpropd  20260  rng1nfld  20265  fldsdrgfld  20321  primefld  20328  fldidom  20812  fldidomOLD  20813  fiidomfld  20816  refld  21060  frlmphllem  21223  frlmphl  21224  recvs  24546  rrxcph  24793  rrx0  24798  ply1pid  25581  lgseisenlem3  26762  lgseisenlem4  26763  fldgenfld  32158  ofldlt1  32179  ofldchr  32180  subofld  32182  isarchiofld  32183  reofld  32207  rearchi  32209  srafldlvec  32374  rgmoddim  32392  ccfldextrr  32424  fldextsralvec  32431  extdgcl  32432  extdggt0  32433  fldextid  32435  extdgmul  32437  extdg1id  32439  ccfldsrarelvec  32442  qqhrhm  32659  matunitlindflem1  36147  matunitlindflem2  36148  matunitlindf  36149  fldhmf1  40620  flddrngd  40780  ricfld  40781  fldcat  46500  fldcatALTV  46518