Theorem isidom 20656

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  CRingccrg 20167  Domncdomn 20623  IDomncidom 20624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-idom 20627

This theorem is referenced by:  fldidom  20702  fiidomfld  20705  znfld  21513  znidomb  21514  ply1idom  26084  fta1glem1  26127  fta1glem2  26128  fta1g  26129  fta1b  26131  idomrootle  26132  lgsqrlem1  27311  lgsqrlem2  27312  lgsqrlem3  27313  lgsqrlem4  27314  idompropd  33309  subridom  33317  dvdsruasso  33415  qsidomlem1  33482  qsidomlem2  33483  zringidom  33581  r1pid2OLD  33639  idomnnzpownz  42325  idomnnzgmulnz  42326  aks6d1c5lem3  42330  aks6d1c5lem2  42331  deg1gprod  42333  deg1pow  42334  idomodle  43375  proot1mul  43378  proot1hash  43379