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

Theorem isidom 19998
 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 19979 . 2 IDomn = (CRing ∩ Domn)
21elin2 4177 1 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2107  CRingccrg 19220  Domncdomn 19974  IDomncidom 19975 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-in 3946  df-idom 19979 This theorem is referenced by:  fldidom  19999  fiidomfld  20002  znfld  20623  znidomb  20624  recvs  23665  ply1idom  24633  fta1glem1  24674  fta1glem2  24675  fta1g  24676  fta1b  24678  lgsqrlem1  25836  lgsqrlem2  25837  lgsqrlem3  25838  lgsqrlem4  25839  qsidomlem1  30869  qsidomlem2  30870  idomrootle  39656  idomodle  39657  proot1mul  39660  proot1hash  39661
 Copyright terms: Public domain W3C validator