Theorem isidom 20823

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  CRingccrg 20311  Domncdomn 20791  IDomncidom 20792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-idom 20795

This theorem is referenced by:  fldidom  20875  fiidomfld  20878  qsidomlem1  21480  qsidomlem2  21481  znfld  21710  znidomb  21711  ply1idom  26282  fta1glem1  26325  fta1glem2  26326  fta1g  26327  fta1b  26329  idomrootle  26330  lgsqrlem1  27510  lgsqrlem2  27511  lgsqrlem3  27512  lgsqrlem4  27513  idompropd  33601  subridom  33606  dvdsruasso  33698  zringidom  33841  mplidomlem  33917  idomnnzpownz  42899  idomnnzgmulnz  42900  aks6d1c5lem3  42904  aks6d1c5lem2  42905  deg1gprod  42907  deg1pow  42908  idomodle  43918  proot1mul  43921  proot1hash  43922  crngprmringdom  49107  idomcanl  49112  idomcanr  49113