Theorem dfidom2

Description: Alternate definition of the class of integral domains. An integral domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Assertion	dfidom2	Could not format assertion : No typesetting found for |- IDomn = ( PrmRing i^i CRing ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-idom	$$⊢\mathrm{IDomn}=\mathrm{CRing}\cap \mathrm{Domn}$$
2	1	eleq2i	$$⊢x\in \mathrm{IDomn}\leftrightarrow x\in \left(\mathrm{CRing}\cap \mathrm{Domn}\right)$$
3		elin	$$⊢x\in \left(\mathrm{CRing}\cap \mathrm{Domn}\right)\leftrightarrow \left(x\in \mathrm{CRing}\wedge x\in \mathrm{Domn}\right)$$
4	3	biancomi	$$⊢x\in \left(\mathrm{CRing}\cap \mathrm{Domn}\right)\leftrightarrow \left(x\in \mathrm{Domn}\wedge x\in \mathrm{CRing}\right)$$
5	2 4	bitri	$$⊢x\in \mathrm{IDomn}\leftrightarrow \left(x\in \mathrm{Domn}\wedge x\in \mathrm{CRing}\right)$$
6		crngprmringdom	Could not format ( x e. CRing -> ( x e. PrmRing <-> x e. Domn ) ) : No typesetting found for |- ( x e. CRing -> ( x e. PrmRing <-> x e. Domn ) ) with typecode |-
7	6	bicomd	Could not format ( x e. CRing -> ( x e. Domn <-> x e. PrmRing ) ) : No typesetting found for |- ( x e. CRing -> ( x e. Domn <-> x e. PrmRing ) ) with typecode |-
8	5 7	bianim	Could not format ( x e. IDomn <-> ( x e. PrmRing /\ x e. CRing ) ) : No typesetting found for |- ( x e. IDomn <-> ( x e. PrmRing /\ x e. CRing ) ) with typecode |-
9		elin	Could not format ( x e. ( PrmRing i^i CRing ) <-> ( x e. PrmRing /\ x e. CRing ) ) : No typesetting found for |- ( x e. ( PrmRing i^i CRing ) <-> ( x e. PrmRing /\ x e. CRing ) ) with typecode |-
10	8 9	bitr4i	Could not format ( x e. IDomn <-> x e. ( PrmRing i^i CRing ) ) : No typesetting found for |- ( x e. IDomn <-> x e. ( PrmRing i^i CRing ) ) with typecode |-
11	10	eqriv	Could not format IDomn = ( PrmRing i^i CRing ) : No typesetting found for |- IDomn = ( PrmRing i^i CRing ) with typecode |-