Theorem isidom 20610

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20119  Domncdomn 20577  IDomncidom 20578

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-idom 20581

This theorem is referenced by:  fldidom  20656  fiidomfld  20659  znfld  21446  znidomb  21447  ply1idom  26006  fta1glem1  26049  fta1glem2  26050  fta1g  26051  fta1b  26053  idomrootle  26054  lgsqrlem1  27233  lgsqrlem2  27234  lgsqrlem3  27235  lgsqrlem4  27236  idompropd  33201  subridom  33209  dvdsruasso  33329  qsidomlem1  33396  qsidomlem2  33397  zringidom  33495  r1pid2OLD  33547  idomnnzpownz  42093  idomnnzgmulnz  42094  aks6d1c5lem3  42098  aks6d1c5lem2  42099  deg1gprod  42101  deg1pow  42102  idomodle  43153  proot1mul  43156  proot1hash  43157