Theorem isidom 20070

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  CRingccrg 19291  Domncdomn 20046  IDomncidom 20047

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 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-idom 20051

This theorem is referenced by:  fldidom  20071  fiidomfld  20074  znfld  20252  znidomb  20253  recvs  23751  ply1idom  24725  fta1glem1  24766  fta1glem2  24767  fta1g  24768  fta1b  24770  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  qsidomlem1  31036  qsidomlem2  31037  idomrootle  40139  idomodle  40140  proot1mul  40143  proot1hash  40144