MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfld Structured version   Visualization version   GIF version

Theorem isfld 19487
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
StepHypRef Expression
1 df-field 19481 . 2 Field = (DivRing ∩ CRing)
21elin2 4149 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wcel 2115  CRingccrg 19277  DivRingcdr 19478  Fieldcfield 19479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-field 19481
This theorem is referenced by:  fldpropd  19506  primefld  19560  rng1nfld  20027  fldidom  20054  fiidomfld  20057  refld  20739  recrng  20741  frlmphllem  20900  frlmphl  20901  rrxcph  23975  rrx0  23980  ply1pid  24759  lgseisenlem3  25940  lgseisenlem4  25941  ofldlt1  30894  ofldchr  30895  subofld  30897  isarchiofld  30898  reofld  30921  rearchi  30923  srafldlvec  31002  rgmoddim  31019  ccfldextrr  31049  fldextsralvec  31056  extdgcl  31057  extdggt0  31058  fldextid  31060  extdgmul  31062  extdg1id  31064  ccfldsrarelvec  31067  qqhrhm  31238  matunitlindflem1  34935  matunitlindflem2  34936  matunitlindf  34937  fldcat  44525  fldcatALTV  44543
  Copyright terms: Public domain W3C validator