Theorem isidom 20641

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 20612	. 2 ⊢ IDomn = (CRing ∩ Domn)
2	1	elin2 4169	1 ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20150  Domncdomn 20608  IDomncidom 20609

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-idom 20612

This theorem is referenced by:  fldidom  20687  fiidomfld  20690  znfld  21477  znidomb  21478  ply1idom  26037  fta1glem1  26080  fta1glem2  26081  fta1g  26082  fta1b  26084  idomrootle  26085  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  idompropd  33235  subridom  33243  dvdsruasso  33363  qsidomlem1  33430  qsidomlem2  33431  zringidom  33529  r1pid2OLD  33581  idomnnzpownz  42127  idomnnzgmulnz  42128  aks6d1c5lem3  42132  aks6d1c5lem2  42133  deg1gprod  42135  deg1pow  42136  idomodle  43187  proot1mul  43190  proot1hash  43191