Theorem isfld 20890

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  CRingccrg 20360  DivRingcdr 20877  Fieldcfield 20878

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-field 20880

This theorem is used by:  flddrngd  20891  fldcrngd  20892  fldpropd  20924  fldidom  20925  fiidomfld  20928  rng1nfld  20932  fldcat  20936  fldsdrgfld  20951  primefld  20958  ofldlt1  21028  subofld  21030  isfieldidl  21436  ofldchr  21776  refld  21819  frlmphllem  21980  frlmphl  21981  recvs  25356  rrxcph  25602  rrx0  25607  ply1pid  26391  lgseisenlem3  27592  lgseisenlem4  27593  isarchiofld  33583  qfld  33682  fracfld  33693  fldgenfld  33705  cnfldfld  33726  reofld  33727  rearchi  33730  qsfld  33844  srafldlvec  34040  assafld  34091  ccfldextrr  34100  fldextsralvec  34109  extdgcl  34110  extdggt0  34111  fldextid  34113  extdgid  34114  extdgmul  34117  extdg1id  34120  ccfldsrarelvec  34125  2sqr3minply  34234  qqhrhm  34443  matunitlindflem1  38324  matunitlindflem2  38325  matunitlindf  38326  fldhmf1  42915  aks6d1c1p2  42934  aks6d1c2lem4  42952  aks6d1c5lem3  42962  aks6d1c5lem2  42963  aks6d1c6lem1  42995  ricfld  43356  fldcatALTV  49153