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

Metamath Proof Explorer

Theorem subrngss

Description: A subring is a subset. (Contributed by AV, 14-Feb-2025)

		Ref	Expression
	Hypothesis	subrngss.1	$⊢ B = {Base}_{R}$
	Assertion	subrngss	$⊢ A \in SubRng (R) \to A \subseteq B$

Step	Hyp	Ref	Expression
1		subrngss.1	$⊢ B = {Base}_{R}$
2	1	issubrng	$⊢ A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B)$
3	2	simp3bi	$⊢ A \in SubRng (R) \to A \subseteq B$