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 Base R A

Proof

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