subrgrcl

Description: Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014)

		Ref	Expression
	Assertion	subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {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 {Base}_{R} \land 1_{R} \in A))$
4	3	simplbi	$⊢ A \in SubRing (R) \to (R \in Ring \land R ↾_{𝑠} A \in Ring)$
5	4	simpld	$⊢ A \in SubRing (R) \to R \in Ring$

Metamath Proof Explorer