Theorem isidom 20670

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  CRingccrg 20181  Domncdomn 20637  IDomncidom 20638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-idom 20641

This theorem is referenced by:  fldidom  20716  fiidomfld  20719  znfld  21527  znidomb  21528  ply1idom  26098  fta1glem1  26141  fta1glem2  26142  fta1g  26143  fta1b  26145  idomrootle  26146  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  idompropd  33372  subridom  33380  dvdsruasso  33478  qsidomlem1  33545  qsidomlem2  33546  zringidom  33644  r1pid2OLD  33702  idomnnzpownz  42502  idomnnzgmulnz  42503  aks6d1c5lem3  42507  aks6d1c5lem2  42508  deg1gprod  42510  deg1pow  42511  idomodle  43548  proot1mul  43551  proot1hash  43552