Theorem subrgccidom

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

	Ref	Expression
Hypotheses	subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
	subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
Assertion	subrgccidom	⊢ 𝑅 ∈ IDomn

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2		subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
3	1 2	subrgcccrng	⊢ 𝑅 ∈ CRing
4	1 2	subrgccdom	⊢ 𝑅 ∈ Domn
5		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
6	3 4 5	mpbir2an	⊢ 𝑅 ∈ IDomn