Theorem isidom 20702

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  CRingccrg 20215  Domncdomn 20669  IDomncidom 20670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-idom 20673

This theorem is referenced by:  fldidom  20748  fiidomfld  20751  znfld  21540  znidomb  21541  ply1idom  26090  fta1glem1  26133  fta1glem2  26134  fta1g  26135  fta1b  26137  idomrootle  26138  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  idompropd  33339  subridom  33347  dvdsruasso  33445  qsidomlem1  33512  qsidomlem2  33513  zringidom  33611  r1pid2OLD  33669  idomnnzpownz  42571  idomnnzgmulnz  42572  aks6d1c5lem3  42576  aks6d1c5lem2  42577  deg1gprod  42579  deg1pow  42580  idomodle  43619  proot1mul  43622  proot1hash  43623