Theorem isidom 20887

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  CRingccrg 20374  Domncdomn 20855  IDomncidom 20856

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-idom 20859

This theorem is used by:  fldidom  20939  fiidomfld  20942  qsidomlem1  21544  qsidomlem2  21545  znfld  21774  znidomb  21775  ply1idom  26351  fta1glem1  26394  fta1glem2  26395  fta1g  26396  fta1b  26398  idomrootle  26399  lgsqrlem1  27583  lgsqrlem2  27584  lgsqrlem3  27585  lgsqrlem4  27586  idompropd  33722  subridom  33727  dvdsruasso  33819  zringidom  33962  mplidomlem  34038  idomnnzpownz  42999  idomnnzgmulnz  43000  aks6d1c5lem3  43004  aks6d1c5lem2  43005  deg1gprod  43007  deg1pow  43008  idomodle  44033  proot1mul  44036  proot1hash  44037  crngprmringdom  49258  idomcanl  49263  idomcanr  49264