Theorem ressid

Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypothesis	ressid.1	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressid	$$⊢W\in X\to W{\upharpoonright }_{𝑠}B=W$$

Proof

Step	Hyp	Ref	Expression
1		ressid.1	$$⊢B={\mathrm{Base}}_W$$
2		ssid	$$⊢B\subseteq B$$
3	1	fvexi	$$⊢B\in \mathrm{V}$$
4		eqid	$$⊢W{\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}B$$
5	4 1	ressid2	$$⊢\left(B\subseteq B\wedge W\in X\wedge B\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}B=W$$
6	2 3 5	mp3an13	$$⊢W\in X\to W{\upharpoonright }_{𝑠}B=W$$