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

Theorem isidom 20150
 Description: An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isidom (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

Proof of Theorem isidom
StepHypRef Expression
1 df-idom 20131 . 2 IDomn = (CRing ∩ Domn)
21elin2 4104 1 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  CRingccrg 19371  Domncdomn 20126  IDomncidom 20127 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-idom 20131 This theorem is referenced by:  fldidom  20151  fiidomfld  20154  znfld  20333  znidomb  20334  recvs  23852  ply1idom  24829  fta1glem1  24870  fta1glem2  24871  fta1g  24872  fta1b  24874  lgsqrlem1  26034  lgsqrlem2  26035  lgsqrlem3  26036  lgsqrlem4  26037  qsidomlem1  31153  qsidomlem2  31154  idomrootle  40540  idomodle  40541  proot1mul  40544  proot1hash  40545
 Copyright terms: Public domain W3C validator