Theorem isidom 20150

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  CRingccrg 19371  Domncdomn 20126  IDomncidom 20127

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-idom 20131

This theorem is referenced by:  fldidom  20151  fiidomfld  20154  znfld  20333  znidomb  20334  recvs  23852  ply1idom  24829  fta1glem1  24870  fta1glem2  24871  fta1g  24872  fta1b  24874  lgsqrlem1  26034  lgsqrlem2  26035  lgsqrlem3  26036  lgsqrlem4  26037  qsidomlem1  31153  qsidomlem2  31154  idomrootle  40540  idomodle  40541  proot1mul  40544  proot1hash  40545