Theorem isidom 21208

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2098  CRingccrg 20131  Domncdomn 21182  IDomncidom 21183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948  df-idom 21187

This theorem is referenced by:  fldidom  21209  fldidomOLD  21210  fiidomfld  21213  znfld  21425  znidomb  21426  recvsOLD  24998  ply1idom  25984  fta1glem1  26025  fta1glem2  26026  fta1g  26027  fta1b  26029  lgsqrlem1  27198  lgsqrlem2  27199  lgsqrlem3  27200  lgsqrlem4  27201  dvdsruasso  32962  qsidomlem1  33043  qsidomlem2  33044  r1pid2  33148  idomrootle  42451  idomodle  42452  proot1mul  42455  proot1hash  42456