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

Theorem isidom 17502
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 17482 . 2  |- IDomn  =  (
CRing  i^i Domn )
21elin2 3652 1  |-  ( R  e. IDomn 
<->  ( R  e.  CRing  /\  R  e. Domn ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1758   CRingccrg 16772  Domncdomn 17477  IDomncidom 17478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446  df-idom 17482
This theorem is referenced by:  fldidom  17503  fiidomfld  17506  znfld  18121  znidomb  18122  ply1idom  21732  fta1glem1  21773  fta1glem2  21774  fta1g  21775  fta1b  21777  lgsqrlem1  22816  lgsqrlem2  22817  lgsqrlem3  22818  lgsqrlem4  22819  idomrootle  29728  idomodle  29729  proot1mul  29732  proot1hash  29736
  Copyright terms: Public domain W3C validator