Theorem isidom 20640

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  CRingccrg 20152  Domncdomn 20607  IDomncidom 20608

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-idom 20611

This theorem is referenced by:  fldidom  20686  fiidomfld  20689  znfld  21497  znidomb  21498  ply1idom  26057  fta1glem1  26100  fta1glem2  26101  fta1g  26102  fta1b  26104  idomrootle  26105  lgsqrlem1  27284  lgsqrlem2  27285  lgsqrlem3  27286  lgsqrlem4  27287  idompropd  33244  subridom  33252  dvdsruasso  33350  qsidomlem1  33417  qsidomlem2  33418  zringidom  33516  r1pid2OLD  33569  idomnnzpownz  42235  idomnnzgmulnz  42236  aks6d1c5lem3  42240  aks6d1c5lem2  42241  deg1gprod  42243  deg1pow  42244  idomodle  43294  proot1mul  43297  proot1hash  43298