Theorem isfld 20904

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  CRingccrg 20374  DivRingcdr 20891  Fieldcfield 20892

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-field 20894

This theorem is used by:  flddrngd  20905  fldcrngd  20906  fldpropd  20938  fldidom  20939  fiidomfld  20942  rng1nfld  20946  fldcat  20950  fldsdrgfld  20965  primefld  20972  ofldlt1  21042  subofld  21044  isfieldidl  21450  ofldchr  21790  refld  21833  frlmphllem  21994  frlmphl  21995  matunitlindflem1  22902  matunitlindflem2  22903  matunitlindf  22904  recvs  25375  rrxcph  25621  rrx0  25626  ply1pid  26409  lgseisenlem3  27614  lgseisenlem4  27615  isarchiofld  33640  qfld  33739  fracfld  33750  fldgenfld  33762  cnfldfld  33783  reofld  33784  rearchi  33787  qsfld  33901  srafldlvec  34097  assafld  34148  ccfldextrr  34157  fldextsralvec  34166  extdgcl  34167  extdggt0  34168  fldextid  34170  extdgid  34171  extdgmul  34174  extdg1id  34177  ccfldsrarelvec  34182  2sqr3minply  34291  qqhrhm  34500  fldhmf1  42957  aks6d1c1p2  42976  aks6d1c2lem4  42994  aks6d1c5lem3  43004  aks6d1c5lem2  43005  aks6d1c6lem1  43037  ricfld  43413  fldcatALTV  49247  veroquadmodzerod  50818  veroquadnolindfd  50819  veroquaddetzerod  50820