Theorem isidom 20670

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2107  CRingccrg 20179  Domncdomn 20637  IDomncidom 20638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-in 3931  df-idom 20641

This theorem is referenced by:  fldidom  20716  fiidomfld  20719  znfld  21506  znidomb  21507  recvsOLD  25083  ply1idom  26067  fta1glem1  26110  fta1glem2  26111  fta1g  26112  fta1b  26114  idomrootle  26115  lgsqrlem1  27293  lgsqrlem2  27294  lgsqrlem3  27295  lgsqrlem4  27296  idompropd  33190  subridom  33198  dvdsruasso  33318  qsidomlem1  33385  qsidomlem2  33386  zringidom  33484  r1pid2OLD  33534  idomnnzpownz  42067  idomnnzgmulnz  42068  aks6d1c5lem3  42072  aks6d1c5lem2  42073  deg1gprod  42075  deg1pow  42076  idomodle  43140  proot1mul  43143  proot1hash  43144