Theorem isidom 20985

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  CRingccrg 20469  Domncdomn 20953  IDomncidom 20954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-idom 20957

This theorem is used by:  fldidom  21038  fiidomfld  21041  qsidomlem1  21645  qsidomlem2  21646  znfld  21875  znidomb  21876  ply1idom  26452  fta1glem1  26495  fta1glem2  26496  fta1g  26497  fta1b  26499  idomrootle  26500  lgsqrlem1  27682  lgsqrlem2  27683  lgsqrlem3  27684  lgsqrlem4  27685  idompropd  33892  subridom  33897  dvdsruasso  33990  zringidom  34133  mplidomlem  34209  idomnnzpownz  43319  idomnnzgmulnz  43320  aks6d1c5lem3  43324  aks6d1c5lem2  43325  deg1gprod  43327  deg1pow  43328  idomodle  44330  proot1mul  44333  proot1hash  44334  crngprmringdom  49575  idomcanl  49580  idomcanr  49581