Metamath Proof Explorer


Theorem ressbasss

Description: The base set of a restriction is a subset of the base set of the original structure. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by SN, 25-Feb-2025)

Ref Expression
Hypotheses ressbas.r R = W 𝑠 A
ressbas.b B = Base W
Assertion ressbasss Base R B

Proof

Step Hyp Ref Expression
1 ressbas.r R = W 𝑠 A
2 ressbas.b B = Base W
3 1 2 ressbasssg Base R A B
4 inss2 A B B
5 3 4 sstri Base R B