Theorem isidom 20645

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20154  Domncdomn 20612  IDomncidom 20613

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 3446  df-in 3918  df-idom 20616

This theorem is referenced by:  fldidom  20691  fiidomfld  20694  znfld  21502  znidomb  21503  ply1idom  26063  fta1glem1  26106  fta1glem2  26107  fta1g  26108  fta1b  26110  idomrootle  26111  lgsqrlem1  27290  lgsqrlem2  27291  lgsqrlem3  27292  lgsqrlem4  27293  idompropd  33244  subridom  33252  dvdsruasso  33349  qsidomlem1  33416  qsidomlem2  33417  zringidom  33515  r1pid2OLD  33567  idomnnzpownz  42113  idomnnzgmulnz  42114  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  deg1pow  42122  idomodle  43173  proot1mul  43176  proot1hash  43177