Theorem isidom 20079

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  CRingccrg 19300  Domncdomn 20055  IDomncidom 20056

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-idom 20060

This theorem is referenced by:  fldidom  20080  fiidomfld  20083  znfld  20709  znidomb  20710  recvs  23752  ply1idom  24720  fta1glem1  24761  fta1glem2  24762  fta1g  24763  fta1b  24765  lgsqrlem1  25924  lgsqrlem2  25925  lgsqrlem3  25926  lgsqrlem4  25927  qsidomlem1  30967  qsidomlem2  30968  idomrootle  39802  idomodle  39803  proot1mul  39806  proot1hash  39807