Database
BASIC ALGEBRAIC STRUCTURES
Rings
Subrings
Subrings of non-unital rings
subrngss
Next ⟩
subrngid
Metamath Proof Explorer
Ascii
Unicode
Theorem
subrngss
Description:
A subring is a subset.
(Contributed by
AV
, 14-Feb-2025)
Ref
Expression
Hypothesis
subrngss.1
⊢
B
=
Base
R
Assertion
subrngss
⊢
A
∈
SubRng
⁡
R
→
A
⊆
B
Proof
Step
Hyp
Ref
Expression
1
subrngss.1
⊢
B
=
Base
R
2
1
issubrng
⊢
A
∈
SubRng
⁡
R
↔
R
∈
Rng
∧
R
↾
𝑠
A
∈
Rng
∧
A
⊆
B
3
2
simp3bi
⊢
A
∈
SubRng
⁡
R
→
A
⊆
B