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

Metamath Proof Explorer

Theorem subrgss

Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014)

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

Step	Hyp	Ref	Expression
1		subrgss.1	$⊢ B = {Base}_{R}$
2		eqid	$⊢ 1_{R} = 1_{R}$
3	1 2	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land 1_{R} \in A))$
4	3	simprbi	$⊢ A \in SubRing (R) \to (A \subseteq B \land 1_{R} \in A)$
5	4	simpld	$⊢ A \in SubRing (R) \to A \subseteq B$