Theorem isidom 20725

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20231  Domncdomn 20692  IDomncidom 20693

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-idom 20696

This theorem is referenced by:  fldidom  20771  fldidomOLD  20772  fiidomfld  20775  znfld  21579  znidomb  21580  recvsOLD  25180  ply1idom  26164  fta1glem1  26207  fta1glem2  26208  fta1g  26209  fta1b  26211  idomrootle  26212  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  idompropd  33281  subridom  33289  dvdsruasso  33413  qsidomlem1  33480  qsidomlem2  33481  zringidom  33579  r1pid2OLD  33629  idomnnzpownz  42133  idomnnzgmulnz  42134  aks6d1c5lem3  42138  aks6d1c5lem2  42139  deg1gprod  42141  deg1pow  42142  idomodle  43203  proot1mul  43206  proot1hash  43207