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 \in Rng \to B \in SubRng (R)$

Step	Hyp	Ref	Expression
1		subrngss.1	$⊢ B = {Base}_{R}$
2		id	$⊢ R \in Rng \to R \in Rng$
3	1	ressid	$⊢ R \in Rng \to R ↾_{𝑠} B = R$
4	3 2	eqeltrd	$⊢ R \in Rng \to R ↾_{𝑠} B \in Rng$
5		ssidd	$⊢ R \in Rng \to B \subseteq B$
6	1	issubrng	$⊢ B \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} B \in Rng \land B \subseteq B)$
7	2 4 5 6	syl3anbrc	$⊢ R \in Rng \to B \in SubRng (R)$

Metamath Proof Explorer