Theorem ringidcld

Description: The unity element of a ring belongs to the base set of the ring, deduction version. (Contributed by SN, 16-Oct-2025)

	Ref	Expression
Hypotheses	ringidcl.b	$$⊢B={\mathrm{Base}}_R$$
	ringidcl.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ringidcld.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	ringidcld	$$⊢\phi \to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		ringidcl.b	$$⊢B={\mathrm{Base}}_R$$
2		ringidcl.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		ringidcld.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4	1 2	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
5	3 4	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$