This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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} \subseteq A$

Step	Hyp	Ref	Expression
1		ressbasss2.r	$⊢ R = W ↾_{𝑠} A$
2		eqid	$⊢ {Base}_{W} = {Base}_{W}$
3	1 2	ressbasssg	$⊢ {Base}_{R} \subseteq A \cap {Base}_{W}$
4		inss1	$⊢ A \cap {Base}_{W} \subseteq A$
5	3 4	sstri	$⊢ {Base}_{R} \subseteq A$