Theorem isidom 20697

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  CRingccrg 20206  Domncdomn 20664  IDomncidom 20665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-idom 20668

This theorem is referenced by:  fldidom  20743  fiidomfld  20746  znfld  21535  znidomb  21536  ply1idom  26108  fta1glem1  26151  fta1glem2  26152  fta1g  26153  fta1b  26155  idomrootle  26156  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  idompropd  33359  subridom  33367  dvdsruasso  33468  qsidomlem1  33535  qsidomlem2  33536  zringidom  33634  r1pid2OLD  33692  mplidomlem  33711  idomnnzpownz  42617  idomnnzgmulnz  42618  aks6d1c5lem3  42622  aks6d1c5lem2  42623  deg1gprod  42625  deg1pow  42626  idomodle  43636  proot1mul  43639  proot1hash  43640