MPE Home 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