Theorem isfld 21002

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  CRingccrg 20469  DivRingcdr 20989  Fieldcfield 20990

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-field 20992

This theorem is used by:  flddrngd  21003  fldcrngd  21004  fldpropd  21037  fldidom  21038  fiidomfld  21041  rng1nfld  21045  fldcat  21049  fldsdrgfld  21064  primefld  21071  ofldlt1  21141  subofld  21143  isfieldidl  21549  ofldchr  21891  refld  21934  frlmphllem  22095  frlmphl  22096  matunitlindflem1  23003  matunitlindflem2  23004  matunitlindf  23005  recvs  25476  rrxcph  25722  rrx0  25727  ply1pid  26510  lgseisenlem3  27713  lgseisenlem4  27714  isarchiofld  33810  qfld  33909  fracfld  33920  fldgenfld  33932  cnfldfld  33953  reofld  33954  rearchi  33957  qsfld  34072  srafldlvec  34268  assafld  34319  ccfldextrr  34328  fldextsralvec  34337  extdgcl  34338  extdggt0  34339  fldextid  34341  extdgid  34342  extdgmul  34345  extdg1id  34348  ccfldsrarelvec  34353  2sqr3minply  34462  qqhrhm  34671  fldhmf1  43277  aks6d1c1p2  43296  aks6d1c2lem4  43314  aks6d1c5lem3  43324  aks6d1c5lem2  43325  aks6d1c6lem1  43357  ricfld  43731  fldcatALTV  49564  veroquadmodzerod  51195  veroquadnolindfd  51196  veroquaddetzerod  51197