Theorem subrngid

Description: Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Hypothesis	subrngss.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	subrngid	Could not format assertion : No typesetting found for |- ( R e. Rng -> B e. ( SubRng ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngss.1	$$⊢B={\mathrm{Base}}_R$$
2		id	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Rng}$$
3	1	ressid	$$⊢R\in \mathrm{Rng}\to R{\upharpoonright }_{𝑠}B=R$$
4	3 2	eqeltrd	$$⊢R\in \mathrm{Rng}\to R{\upharpoonright }_{𝑠}B\in \mathrm{Rng}$$
5		ssidd	$$⊢R\in \mathrm{Rng}\to B\subseteq B$$
6	1	issubrng	Could not format ( B e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s B ) e. Rng /\ B C_ B ) ) : No typesetting found for |- ( B e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s B ) e. Rng /\ B C_ B ) ) with typecode |-
7	2 4 5 6	syl3anbrc	Could not format ( R e. Rng -> B e. ( SubRng ` R ) ) : No typesetting found for |- ( R e. Rng -> B e. ( SubRng ` R ) ) with typecode |-