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 |`s A )
Assertion	ressbasss2	|- ( Base ` R ) C_ A

Proof

Step	Hyp	Ref	Expression
1		ressbasss2.r	|- R = ( W |`s A )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3	1 2	ressbasssg	|- ( Base ` R ) C_ ( A i^i ( Base ` W ) )
4		inss1	|- ( A i^i ( Base ` W ) ) C_ A
5	3 4	sstri	|- ( Base ` R ) C_ A