Theorem isfld 20840

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  CRingccrg 20311  DivRingcdr 20827  Fieldcfield 20828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-field 20830

This theorem is referenced by:  flddrngd  20841  fldcrngd  20842  fldpropd  20874  fldidom  20875  fiidomfld  20878  rng1nfld  20882  fldcat  20886  fldsdrgfld  20901  primefld  20908  ofldlt1  20978  subofld  20980  isfieldidl  21386  ofldchr  21726  refld  21769  frlmphllem  21930  frlmphl  21931  recvs  25305  rrxcph  25551  rrx0  25556  ply1pid  26340  lgseisenlem3  27541  lgseisenlem4  27542  isarchiofld  33519  qfld  33618  fracfld  33629  fldgenfld  33641  cnfldfld  33662  reofld  33663  rearchi  33666  qsfld  33780  srafldlvec  33976  assafld  34027  ccfldextrr  34036  fldextsralvec  34045  extdgcl  34046  extdggt0  34047  fldextid  34049  extdgid  34050  extdgmul  34053  extdg1id  34056  ccfldsrarelvec  34061  2sqr3minply  34170  qqhrhm  34379  matunitlindflem1  38267  matunitlindflem2  38268  matunitlindf  38269  fldhmf1  42857  aks6d1c1p2  42876  aks6d1c2lem4  42894  aks6d1c5lem3  42904  aks6d1c5lem2  42905  aks6d1c6lem1  42937  ricfld  43298  fldcatALTV  49096