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	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
2	1	subrgss	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$