Theorem isidom 20575

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  CRingccrg 19784  Domncdomn 20551  IDomncidom 20552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-idom 20556

This theorem is referenced by:  fldidom  20576  fldidomOLD  20577  fiidomfld  20580  znfld  20768  znidomb  20769  recvsOLD  24310  ply1idom  25289  fta1glem1  25330  fta1glem2  25331  fta1g  25332  fta1b  25334  lgsqrlem1  26494  lgsqrlem2  26495  lgsqrlem3  26496  lgsqrlem4  26497  qsidomlem1  31628  qsidomlem2  31629  idomrootle  41020  idomodle  41021  proot1mul  41024  proot1hash  41025