Theorem isidom 20914

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  CRingccrg 20050  Domncdomn 20888  IDomncidom 20889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-idom 20893

This theorem is referenced by:  fldidom  20915  fldidomOLD  20916  fiidomfld  20919  znfld  21107  znidomb  21108  recvsOLD  24654  ply1idom  25633  fta1glem1  25674  fta1glem2  25675  fta1g  25676  fta1b  25678  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgsqrlem4  26841  dvdsruasso  32478  qsidomlem1  32559  qsidomlem2  32560  idomrootle  41922  idomodle  41923  proot1mul  41926  proot1hash  41927