This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrngid

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

Ref Expression
Hypothesis subrngss.1 ⊢ B = Base R
Assertion subrngid ⊢ R ∈ Rng → B ∈ SubRng ⁡ R

Proof

Step Hyp Ref Expression
1 subrngss.1 ⊢ B = Base R
2 id ⊢ R ∈ Rng → R ∈ Rng
3 1 ressid ⊢ R ∈ Rng → R ↾ 𝑠 B = R
4 3 2 eqeltrd ⊢ R ∈ Rng → R ↾ 𝑠 B ∈ Rng
5 ssidd ⊢ R ∈ Rng → B ⊆ B
6 1 issubrng ⊢ B ∈ SubRng ⁡ R ↔ R ∈ Rng ∧ R ↾ 𝑠 B ∈ Rng ∧ B ⊆ B
7 2 4 5 6 syl3anbrc ⊢ R ∈ Rng → B ∈ SubRng ⁡ R