Theorem isfld 20993

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 20983	. 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 20460  DivRingcdr 20980  Fieldcfield 20981

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-field 20983

This theorem is used by:  flddrngd  20994  fldcrngd  20995  fldpropd  21028  fldidom  21029  fiidomfld  21032  rng1nfld  21036  fldcat  21040  fldsdrgfld  21055  primefld  21062  ofldlt1  21132  subofld  21134  isfieldidl  21540  ofldchr  21882  refld  21925  frlmphllem  22086  frlmphl  22087  matunitlindflem1  22994  matunitlindflem2  22995  matunitlindf  22996  recvs  25467  rrxcph  25713  rrx0  25718  ply1pid  26501  lgseisenlem3  27704  lgseisenlem4  27705  isarchiofld  33760  qfld  33859  fracfld  33870  fldgenfld  33882  cnfldfld  33903  reofld  33904  rearchi  33907  qsfld  34022  srafldlvec  34218  assafld  34269  ccfldextrr  34278  fldextsralvec  34287  extdgcl  34288  extdggt0  34289  fldextid  34291  extdgid  34292  extdgmul  34295  extdg1id  34298  ccfldsrarelvec  34303  2sqr3minply  34412  qqhrhm  34621  fldhmf1  43140  aks6d1c1p2  43159  aks6d1c2lem4  43177  aks6d1c5lem3  43187  aks6d1c5lem2  43188  aks6d1c6lem1  43220  ricfld  43594  fldcatALTV  49427  veroquadmodzerod  50983  veroquadnolindfd  50984  veroquaddetzerod  50985