Theorem ressbas2

Description: Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
	ressbas.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_R$$

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		ressbas.b	$$⊢B={\mathrm{Base}}_W$$
3		dfss2	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
4	3	biimpi	$$⊢A\subseteq B\to A\cap B=A$$
5	2	fvexi	$$⊢B\in \mathrm{V}$$
6	5	ssex	$$⊢A\subseteq B\to A\in \mathrm{V}$$
7	1 2	ressbas	$$⊢A\in \mathrm{V}\to A\cap B={\mathrm{Base}}_R$$
8	6 7	syl	$$⊢A\subseteq B\to A\cap B={\mathrm{Base}}_R$$
9	4 8	eqtr3d	$$⊢A\subseteq B\to A={\mathrm{Base}}_R$$