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

Metamath Proof Explorer

Theorem subrngrcl

Description: Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025)

		Ref	Expression
	Assertion	subrngrcl	$⊢ A \in SubRng (R) \to R \in Rng$

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