Theorem subrngid

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

	Ref	Expression
Hypothesis	subrngss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	subrngid	⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		subrngss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		id	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Rng )
3	1	ressid	⊢ ( 𝑅 ∈ Rng → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
4	3 2	eqeltrd	⊢ ( 𝑅 ∈ Rng → ( 𝑅 ↾s 𝐵 ) ∈ Rng )
5		ssidd	⊢ ( 𝑅 ∈ Rng → 𝐵 ⊆ 𝐵 )
6	1	issubrng	⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐵 ) ∈ Rng ∧ 𝐵 ⊆ 𝐵 ) )
7	2 4 5 6	syl3anbrc	⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ ( SubRng ‘ 𝑅 ) )