Theorem isidom 20747

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20261  Domncdomn 20714  IDomncidom 20715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-idom 20718

This theorem is referenced by:  fldidom  20793  fldidomOLD  20794  fiidomfld  20797  znfld  21602  znidomb  21603  recvsOLD  25199  ply1idom  26184  fta1glem1  26227  fta1glem2  26228  fta1g  26229  fta1b  26231  idomrootle  26232  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  subridom  33255  dvdsruasso  33378  qsidomlem1  33445  qsidomlem2  33446  zringidom  33544  r1pid2OLD  33594  idomnnzpownz  42089  idomnnzgmulnz  42090  aks6d1c5lem3  42094  aks6d1c5lem2  42095  deg1gprod  42097  deg1pow  42098  idomodle  43152  proot1mul  43155  proot1hash  43156