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

Theorem isfld 18527
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 18521 . 2 Field = (DivRing ∩ CRing)
21elin2 3762 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wcel 1976  CRingccrg 18319  DivRingcdr 18518  Fieldcfield 18519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-field 18521
This theorem is referenced by:  fldpropd  18546  rng1nfld  19047  fldidom  19074  fiidomfld  19077  refld  19731  recrng  19733  frlmphllem  19885  frlmphl  19886  rrxcph  22932  ply1pid  23687  lgseisenlem3  24846  lgseisenlem4  24847  ofldlt1  28937  ofldchr  28938  subofld  28940  isarchiofld  28941  reofld  28964  rearchi  28966  qqhrhm  29154  matunitlindflem1  32358  matunitlindflem2  32359  matunitlindf  32360  fldcat  41855  fldcatALTV  41874
  Copyright terms: Public domain W3C validator