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

Theorem isidom 20790
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 20771 . 2 IDomn = (CRing ∩ Domn)
21elin2 4158 1 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2107  CRingccrg 19970  Domncdomn 20766  IDomncidom 20767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-idom 20771
This theorem is referenced by:  fldidom  20791  fldidomOLD  20792  fiidomfld  20795  znfld  20983  znidomb  20984  recvsOLD  24526  ply1idom  25505  fta1glem1  25546  fta1glem2  25547  fta1g  25548  fta1b  25550  lgsqrlem1  26710  lgsqrlem2  26711  lgsqrlem3  26712  lgsqrlem4  26713  qsidomlem1  32273  qsidomlem2  32274  idomrootle  41565  idomodle  41566  proot1mul  41569  proot1hash  41570
  Copyright terms: Public domain W3C validator