Theorem subrgccsscc

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

	Ref	Expression
Assertion	subrgccsscc	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
2	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )