Theorem isidom 21027

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  CRingccrg 20511  Domncdomn 20995  IDomncidom 20996

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-idom 20999

This theorem is used by:  fldidom  21080  fiidomfld  21083  qsidomlem1  21687  qsidomlem2  21688  znfld  21921  znidomb  21922  ply1idom  26498  fta1glem1  26541  fta1glem2  26542  fta1g  26543  fta1b  26545  idomrootle  26546  lgsqrlem1  27730  lgsqrlem2  27731  lgsqrlem3  27732  lgsqrlem4  27733  idompropd  33941  subridom  33946  zringidom  33957  dvdsruasso  34044  mplidomlem  34270  idomnnzpownz  43448  idomnnzgmulnz  43449  aks6d1c5lem3  43453  aks6d1c5lem2  43454  deg1gprod  43456  deg1pow  43457  idomodle  44454  proot1mul  44457  proot1hash  44458  subrgccidom  49710  crngprmringdom  49770  idomcanl  49775  idomcanr  49776