Theorem isidom 21122

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  CRingccrg 20128  Domncdomn 21096  IDomncidom 21097

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 3955  df-idom 21101

This theorem is referenced by:  fldidom  21123  fldidomOLD  21124  fiidomfld  21127  znfld  21335  znidomb  21336  recvsOLD  24887  ply1idom  25866  fta1glem1  25907  fta1glem2  25908  fta1g  25909  fta1b  25911  lgsqrlem1  27073  lgsqrlem2  27074  lgsqrlem3  27075  lgsqrlem4  27076  dvdsruasso  32752  qsidomlem1  32833  qsidomlem2  32834  r1pid2  32942  idomrootle  42239  idomodle  42240  proot1mul  42243  proot1hash  42244