Theorem isidom 20658

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  CRingccrg 20169  Domncdomn 20625  IDomncidom 20626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-idom 20629

This theorem is referenced by:  fldidom  20704  fiidomfld  20707  znfld  21515  znidomb  21516  ply1idom  26086  fta1glem1  26129  fta1glem2  26130  fta1g  26131  fta1b  26133  idomrootle  26134  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  idompropd  33360  subridom  33368  dvdsruasso  33466  qsidomlem1  33533  qsidomlem2  33534  zringidom  33632  r1pid2OLD  33690  idomnnzpownz  42396  idomnnzgmulnz  42397  aks6d1c5lem3  42401  aks6d1c5lem2  42402  deg1gprod  42404  deg1pow  42405  idomodle  43443  proot1mul  43446  proot1hash  43447