Theorem isidom 20775

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  CRingccrg 20284  Domncdomn 20742  IDomncidom 20743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-idom 20746

This theorem is referenced by:  fldidom  20821  fiidomfld  20824  znfld  21612  znidomb  21613  ply1idom  26185  fta1glem1  26228  fta1glem2  26229  fta1g  26230  fta1b  26232  idomrootle  26233  lgsqrlem1  27410  lgsqrlem2  27411  lgsqrlem3  27412  lgsqrlem4  27413  idompropd  33462  subridom  33470  dvdsruasso  33571  qsidomlem1  33639  qsidomlem2  33640  zringidom  33747  r1pid2OLD  33805  mplidomlem  33824  idomnnzpownz  42749  idomnnzgmulnz  42750  aks6d1c5lem3  42754  aks6d1c5lem2  42755  deg1gprod  42757  deg1pow  42758  idomodle  43768  proot1mul  43771  proot1hash  43772