Metamath Proof Explorer

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 e. ( SubRng ` R ) -> A C_ B )

Proof

Step Hyp Ref Expression
1 subrngss.1 
 |-  B = ( Base ` R )
2 1 issubrng 
 |-  ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) )
3 2 simp3bi 
 |-  ( A e. ( SubRng ` R ) -> A C_ B )