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

Theorem isidom 16365
Description: An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isidom  |-  ( R  e. IDomn 
<->  ( R  e.  CRing  /\  R  e. Domn ) )

Proof of Theorem isidom
StepHypRef Expression
1 df-idom 16346 . 2  |- IDomn  =  (
CRing  i^i Domn )
21elin2 3532 1  |-  ( R  e. IDomn 
<->  ( R  e.  CRing  /\  R  e. Domn ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1726   CRingccrg 15662  Domncdomn 16341  IDomncidom 16342
This theorem is referenced by:  fldidom  16366  fiidomfld  16369  znfld  16842  znidomb  16843  ply1idom  20048  fta1glem1  20089  fta1glem2  20090  fta1g  20091  fta1b  20093  lgsqrlem1  21126  lgsqrlem2  21127  lgsqrlem3  21128  lgsqrlem4  21129  idomrootle  27489  idomodle  27490  proot1mul  27493  proot1hash  27497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328  df-idom 16346
  Copyright terms: Public domain W3C validator