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

Theorem isidom 20725
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 20696 . 2 IDomn = (CRing ∩ Domn)
21elin2 4203 1 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2108  CRingccrg 20231  Domncdomn 20692  IDomncidom 20693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-idom 20696
This theorem is referenced by:  fldidom  20771  fldidomOLD  20772  fiidomfld  20775  znfld  21579  znidomb  21580  recvsOLD  25180  ply1idom  26164  fta1glem1  26207  fta1glem2  26208  fta1g  26209  fta1b  26211  idomrootle  26212  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  idompropd  33281  subridom  33289  dvdsruasso  33413  qsidomlem1  33480  qsidomlem2  33481  zringidom  33579  r1pid2OLD  33629  idomnnzpownz  42133  idomnnzgmulnz  42134  aks6d1c5lem3  42138  aks6d1c5lem2  42139  deg1gprod  42141  deg1pow  42142  idomodle  43203  proot1mul  43206  proot1hash  43207
  Copyright terms: Public domain W3C validator