Theorem subrngrng

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

	Ref	Expression
Hypothesis	subrngrng.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
Assertion	subrngrng	Could not format assertion : No typesetting found for |- ( A e. ( SubRng ` R ) -> S e. Rng ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngrng.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		simp2	$$⊢\left(R\in \mathrm{Rng}\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{Rng}\wedge A\subseteq {\mathrm{Base}}_R\right)\to R{\upharpoonright }_{𝑠}A\in \mathrm{Rng}$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3	issubrng	Could not format ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) ) with typecode |-
5	1	eleq1i	$$⊢S\in \mathrm{Rng}\leftrightarrow R{\upharpoonright }_{𝑠}A\in \mathrm{Rng}$$
6	2 4 5	3imtr4i	Could not format ( A e. ( SubRng ` R ) -> S e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> S e. Rng ) with typecode |-