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

Theorem isidom 20741
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 20712 . 2 IDomn = (CRing ∩ Domn)
21elin2 4212 1 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2105  CRingccrg 20251  Domncdomn 20708  IDomncidom 20709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-idom 20712
This theorem is referenced by:  fldidom  20787  fldidomOLD  20788  fiidomfld  20791  znfld  21596  znidomb  21597  recvsOLD  25193  ply1idom  26178  fta1glem1  26221  fta1glem2  26222  fta1g  26223  fta1b  26225  idomrootle  26226  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  subridom  33269  dvdsruasso  33392  qsidomlem1  33459  qsidomlem2  33460  zringidom  33558  r1pid2OLD  33608  idomnnzpownz  42113  idomnnzgmulnz  42114  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  deg1pow  42122  idomodle  43179  proot1mul  43182  proot1hash  43183
  Copyright terms: Public domain W3C validator