Theorem isidom 20488

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  CRingccrg 19699  Domncdomn 20464  IDomncidom 20465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-idom 20469

This theorem is referenced by:  fldidom  20489  fldidomOLD  20490  fiidomfld  20493  znfld  20680  znidomb  20681  recvs  24215  ply1idom  25194  fta1glem1  25235  fta1glem2  25236  fta1g  25237  fta1b  25239  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  qsidomlem1  31530  qsidomlem2  31531  idomrootle  40936  idomodle  40937  proot1mul  40940  proot1hash  40941