Theorem isidom 20683

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20192  Domncdomn 20650  IDomncidom 20651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-idom 20654

This theorem is referenced by:  fldidom  20729  fiidomfld  20732  znfld  21519  znidomb  21520  recvsOLD  25096  ply1idom  26080  fta1glem1  26123  fta1glem2  26124  fta1g  26125  fta1b  26127  idomrootle  26128  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  idompropd  33218  subridom  33226  dvdsruasso  33346  qsidomlem1  33413  qsidomlem2  33414  zringidom  33512  r1pid2OLD  33564  idomnnzpownz  42091  idomnnzgmulnz  42092  aks6d1c5lem3  42096  aks6d1c5lem2  42097  deg1gprod  42099  deg1pow  42100  idomodle  43162  proot1mul  43165  proot1hash  43166