Theorem isidom 20610

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20119  Domncdomn 20577  IDomncidom 20578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910  df-idom 20581

This theorem is referenced by:  fldidom  20656  fiidomfld  20659  znfld  21467  znidomb  21468  ply1idom  26028  fta1glem1  26071  fta1glem2  26072  fta1g  26073  fta1b  26075  idomrootle  26076  lgsqrlem1  27255  lgsqrlem2  27256  lgsqrlem3  27257  lgsqrlem4  27258  idompropd  33217  subridom  33225  dvdsruasso  33322  qsidomlem1  33389  qsidomlem2  33390  zringidom  33488  r1pid2OLD  33541  idomnnzpownz  42109  idomnnzgmulnz  42110  aks6d1c5lem3  42114  aks6d1c5lem2  42115  deg1gprod  42117  deg1pow  42118  idomodle  43168  proot1mul  43171  proot1hash  43172