Database
BASIC ALGEBRAIC STRUCTURES
Rings
Subrings
Subrings of non-unital rings
subrngrcl
Next ⟩
subrngsubg
Metamath Proof Explorer
Ascii
Unicode
Theorem
subrngrcl
Description:
Reverse closure for a subring predicate.
(Contributed by
AV
, 14-Feb-2025)
Ref
Expression
Assertion
subrngrcl
⊢
A
∈
SubRng
⁡
R
→
R
∈
Rng
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
Base
R
=
Base
R
2
1
issubrng
⊢
A
∈
SubRng
⁡
R
↔
R
∈
Rng
∧
R
↾
𝑠
A
∈
Rng
∧
A
⊆
Base
R
3
2
simp1bi
⊢
A
∈
SubRng
⁡
R
→
R
∈
Rng