Theorem isidom 20808

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

Step	Hyp	Ref	Expression
1		df-idom 20780	. 2 ⊢ IDomn = (CRing ∩ Domn)
2	1	elin2 4164	1 ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  CRingccrg 20315  Domncdomn 20776  IDomncidom 20777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-idom 20780

This theorem is referenced by:  fldidom  20852  fiidomfld  20855  qsidomlem1  21448  qsidomlem2  21449  znfld  21678  znidomb  21679  ply1idom  26250  fta1glem1  26293  fta1glem2  26294  fta1g  26295  fta1b  26297  idomrootle  26298  lgsqrlem1  27475  lgsqrlem2  27476  lgsqrlem3  27477  lgsqrlem4  27478  idompropd  33541  subridom  33546  dvdsruasso  33641  zringidom  33785  mplidomlem  33861  idomnnzpownz  42788  idomnnzgmulnz  42789  aks6d1c5lem3  42793  aks6d1c5lem2  42794  deg1gprod  42796  deg1pow  42797  idomodle  43809  proot1mul  43812  proot1hash  43813  crngprmringdom  48995