Theorem isfld 20049

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2104  CRingccrg 19833  DivRingcdr 20040  Fieldcfield 20041

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-field 20043

This theorem is referenced by:  fldpropd  20068  primefld  20122  rng1nfld  20598  fldidom  20625  fldidomOLD  20626  fiidomfld  20629  refld  20873  recrng  20875  frlmphllem  21036  frlmphl  21037  recvs  24358  rrxcph  24605  rrx0  24610  ply1pid  25393  lgseisenlem3  26574  lgseisenlem4  26575  ofldlt1  31561  ofldchr  31562  subofld  31564  isarchiofld  31565  reofld  31593  rearchi  31595  srafldlvec  31725  rgmoddim  31742  ccfldextrr  31772  fldextsralvec  31779  extdgcl  31780  extdggt0  31781  fldextid  31783  extdgmul  31785  extdg1id  31787  ccfldsrarelvec  31790  qqhrhm  31988  matunitlindflem1  35821  matunitlindflem2  35822  matunitlindf  35823  fldcrngd  40450  prjcrv0  40665  fldcat  45884  fldcatALTV  45902