Theorem subrgccidom

Description: A subring of the complex numbers is an integral domain. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Hypotheses	subrgcccrng.r	|- R = ( CCfld |`s S )
	subrgcccrng.s	|- S e. ( SubRing ` CCfld )
Assertion	subrgccidom	|- R e. IDomn

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	|- R = ( CCfld |`s S )
2		subrgcccrng.s	|- S e. ( SubRing ` CCfld )
3	1 2	subrgcccrng	|- R e. CRing
4	1 2	subrgccdom	|- R e. Domn
5		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
6	3 4 5	mpbir2an	|- R e. IDomn