Metamath Proof Explorer


Theorem ressbasss2

Description: The base set of a restriction to A is a subset of A . (Contributed by SN, 10-Jan-2025)

Ref Expression
Hypothesis ressbasss2.r R=W𝑠A
Assertion ressbasss2 BaseRA

Proof

Step Hyp Ref Expression
1 ressbasss2.r R=W𝑠A
2 eqid BaseW=BaseW
3 1 2 ressbasssg BaseRABaseW
4 inss1 ABaseWA
5 3 4 sstri BaseRA