Theorem isidom 19304

Description: An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)

Assertion

Ref	Expression
isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )

Proof of Theorem isidom

Step	Hyp	Ref	Expression
1		df-idom 19285	. 2 |- IDomn = ( CRing i^i Domn )
2	1	elin2 3801	1 |- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   CRingccrg 18548  Domncdomn 19280  IDomncidom 19281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-idom 19285

This theorem is referenced by:  fldidom  19305  fiidomfld  19308  znfld  19909  znidomb  19910  recvs  22946  ply1idom  23884  fta1glem1  23925  fta1glem2  23926  fta1g  23927  fta1b  23929  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  idomrootle  37773  idomodle  37774  proot1mul  37777  proot1hash  37778